[Merged by Bors] - feat(algebra/order/monoid): generalize, convert to to_additive
and iff of lt_or_lt_of_mul_lt_mul
#13192
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I converted a lemma showing
m + n < a + b → m < a ∨ n < b
to the
to_additive
version of a lemma showingm * n < a * b → m < a ∨ n < b
.I also added a lemma showing
m * n < a * b ↔ m < a ∨ n < b
and itsto_additive
version.