RP Mathbox Ordinals (#4539)

* Rename hypotheses for pren2d.

* RP Mathbox: replace syl5bi with biimtrid

* Add theorems using oF +o to perform an operation isomorphic to natural addition on Cantor normal forms.

* Add a generic closure law for ordinal addition.
Prove statements about ordinal addition being applied to general ordinal-yielding functions.

* Mathbox minimization pass.