Theorem Order.lt_add_one_iff_of_not_isMax'

Modification history

2026-07-07 14:28

Mathlib/Algebra/Order/SuccPred.lean

feat(Order/SuccPred): `succ a ≤ b ↔ a < b` when `b` is not maximal (#41371) …

Added Order.lt_add_one_iff_of_not_isMax'View on Github →