Theorem Order.succ_max

Modification history

2026-02-22 13:15
Mathlib/Order/SuccPred/Basic.lean
chore(Order/SuccPred/Archimedean): use `to_dual` (#34882)
Added Order.succ_maxView on Github →