Theorem WithBot.succ_pred_coe

Modification history

2026-11-10 13:26
Mathlib/Order/SuccPred/WithBot.lean
feat: interaction between `WithBot.succ` and `Order.pred` (#45582)
Added WithBot.succ_pred_coeView on Github →