Theorem Order.succ_le_iff_of_not_isMax'

Modification history

2026-07-07 14:28
Mathlib/Order/SuccPred/Basic.lean
feat(Order/SuccPred): `succ a ≤ b ↔ a < b` when `b` is not maximal (#41371) …
Added Order.succ_le_iff_of_not_isMax'View on Github →