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

src/algebra/ordered_ring.lean

@@ -144,6 +144,10 @@ calc a + (2 + b) ≤ a + (a + a * b) :
       add_le_add_left (add_le_add a2 (le_mul_of_one_le_left b0 (one_le_two.trans a2))) a
              ... ≤ a * (2 + b) : by rw [mul_add, mul_two, add_assoc]
 
+lemma one_le_mul_of_one_le_of_one_le {a b : α} (a1 : 1 ≤ a) (b1 : 1 ≤ b) :
+  (1 : α) ≤ a * b :=
+(mul_one (1 : α)).symm.le.trans (mul_le_mul a1 b1 zero_le_one (zero_le_one.trans a1))
+
 section
 variable [nontrivial α]