[Merged by Bors] - chore: deprecate Ordinal.natCast_succ → Nat.cast_add_one#39643

vihdzp wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

vihdzp:ncsvihdzp/mathlib4:ncsCopy head branch name to clipboard