Theorem Order.le_iff_eq_or_le_pred

Modification history

2025-12-05 23:23
Mathlib/Order/SuccPred/Basic.lean
chore(Order/SuccPred/Basic): use `to_dual` (#32447) …
Deleted Order.le_iff_eq_or_le_predView on Github →
2025-03-04 16:27
Mathlib/Order/SuccPred/Basic.lean
feat: `insert a (Icc (a + 1) b) = Icc a b` (#22559)
Added Order.le_iff_eq_or_le_predView on Github →