Commit 2026-07-07 14:28 6f604786

feat(Data/ENat/Basic): coe versions of m + 1 ≤ n ↔ m < n (#41372) Nat.cast specializations of add_one_le_iff/add_one_le_iff'/lt_add_one_iff' (the lt_add_one_iff version already exists). These are helpful with simp-like tactics which don't like the ≠ ⊤ side condition.