mathlib3

fefe359d - feat(set_theory/principal): prove theorems about additive principal ordinals (#11704)