Theorem WithBot.succ_lt_succ

Modification history

2024-12-20 15:29
Mathlib/Order/SuccPred/WithBot.lean
feat: the successor as a function `WithBot α → α` (#20055) …
Added WithBot.succ_lt_succView on Github →