Commit 2026-02-27 02:54 bce6de5d

View on Github →

refactor: make Order.succ_eq_add_one a simp lemma (#35741) This has been the intention since the SuccAddOrder typeclass was introduced; after #35553, we can finally go ahead with this. A lot of lemmas about ordinals are still stated using succ x instead of x + 1. Fixing this will be the work of many subsequent PRs.

Estimated changes

added theorem Order.add_one_inj
added theorem Cardinal.aleph_add_one
modified theorem Cardinal.aleph_succ
added theorem Cardinal.beth_add_one
modified theorem Cardinal.beth_succ
modified theorem Cardinal.preBeth_succ
added theorem Ordinal.cof_add_one
added theorem Ordinal.cof_one
added theorem Ordinal.lift_add_one
modified theorem Ordinal.lift_succ
added theorem Ordinal.pred_add_one
modified theorem Ordinal.succ_one
added theorem Ordinal.opow_add_one
modified theorem Ordinal.opow_succ
added theorem Ordinal.deriv_add_one
modified theorem Ordinal.toZFSet_succ