Commit 2022-06-03 22:33 00982865

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.