chore: forward port #14324 (#5973)

This is the remainder of the forward port of leanprover-community/mathlib#14324.

See https://leanprover-community.github.io/mathlib-port-status/file/set_theory/ordinal/natural_ops for the relevant #outofsync page.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>