Theorem Order.le_iff_eq_or_succ_le'

Modification history

2025-12-05 23:23
Mathlib/Order/SuccPred/Basic.lean
chore(Order/SuccPred/Basic): use `to_dual` (#32447) …
Added Order.le_iff_eq_or_succ_le'View on Github →