feat(set_theory/ordinal/basic): Turn various lemmas into `simp` (#14075)
feat(set_theory/ordinal/basic): Turn various lemmas into `simp` (#14075)






leanprover-community/mathlib,leanprover-community/mathlib