Commit 2026-11-10 13:26 35d04d09

View on Github →

feat: interaction between WithBot.succ and Order.pred (#45582)

Estimated changes

Modified Mathlib/Order/SuccPred/Basic.lean

added theorem WithTop.succ_coe_eq_top_iff

Modified Mathlib/Order/SuccPred/WithBot.lean

modified theorem WithBot.succ_eq_bot

added theorem WithBot.succ_pred_coe