mathlib

00982865 - feat(set_theory/ordinal/natural_ops): define natural addition (#14291)

feat(set_theory/ordinal/natural_ops): define natural addition (#14291) We define the natural addition operation on ordinals. We prove the basic properties, like commutativity, associativity, and cancellativity. We also provide the type synonym `nat_ordinal` for ordinals with natural operations, which allows us to take full advantage of this rich algebraic structure.