Theorem WithTop.succ_coe_eq_top_iff

Modification history

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