Commit 2026-07-07 14:28 a92c9866

View on Github →

feat(Order/SuccPred): succ a ≤ b ↔ a < b when b is not maximal (#41371) This is succ_le_iff_of_not_isMax' (the unprimed version takes IsMax a instead). Also adds a LinearOrder version with the negated inequalities, versions for SuccAddOrder, and golfs the matching ENat theorems with those.

Estimated changes

Modified Mathlib/Algebra/Order/SuccPred.lean

added theorem Order.add_one_le_iff_of_not_isMax'

added theorem Order.lt_add_one_iff_of_not_isMax'

Modified Mathlib/Data/ENat/Basic.lean

modified theorem ENat.add_one_le_iff'

modified theorem ENat.lt_add_one_iff'

modified theorem ENat.lt_add_one_iff

Modified Mathlib/Order/SuccPred/Basic.lean

modified theorem Order.le_of_lt_succ

added theorem Order.lt_succ_iff_of_not_isMax'

modified theorem Order.lt_succ_iff_of_not_isMax

added theorem Order.succ_le_iff_of_not_isMax'