Commit 2022-04-07 14:25 321d159d

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.