mathlib3

307a456f - refactor(set_theory/ordinal): Add `covariant_class` instances for ordinal addition and multiplication (#11678)

refactor(set_theory/ordinal): Add `covariant_class` instances for ordinal addition and multiplication (#11678) This replaces the old `add_le_add_left`, `add_le_add_right`, `mul_le_mul_left`, `mul_le_mul_right` theorems.