mathlib

b9354dda - feat(algebra/ordered_ring): a product is at least one if both factors are (#6172)

feat(algebra/ordered_ring): a product is at least one if both factors are (#6172) Add single lemma one_le_mul_of_one_le_of_one_le The lemma is stated for an `ordered_semiring`, but only multiplication is used. There does not seem to be an `ordered_monoid` class where this lemma would fit. Relevant Zulip chat: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/ordered_monoid.3F