mathlib3

321d159d - feat(algebra/order/monoid): generalize, convert to `to_additive` and iff of `lt_or_lt_of_mul_lt_mul` (#13192)

feat(algebra/order/monoid): generalize, convert to `to_additive` and iff of `lt_or_lt_of_mul_lt_mul` (#13192) I converted a lemma showing `m + n < a + b → m < a ∨ n < b` to the `to_additive` version of a lemma showing `m * n < a * b → m < a ∨ n < b`. I also added a lemma showing `m * n < a * b ↔ m < a ∨ n < b` and its `to_additive` version.