mathlib3

35cd7c0c - refactor(set_theory/ordinal_arithmetic) Separate `is_normal.lt_iff` (#10745)

refactor(set_theory/ordinal_arithmetic) Separate `is_normal.lt_iff` (#10745) We split off `is_normal.strict_mono` from `is_normal.lt_iff`. The reasoning is that normal functions are usually defined as being strictly monotone, so this should be a separate theorem.