mathlib3

ccbb8487 - feat(set_theory/ordinal_arithmetic): `lt_add_of_limit` (#11748)

feat(set_theory/ordinal_arithmetic): `lt_add_of_limit` (#11748) Both `lt_mul_of_limit` and `lt_opow_of_limit` already existed, so this exclusion is odd to say the least.