feat: Match mathlib#16761 (#840)

* feat: Match mathlib#16761

* fix

Author: YaelDillies

Mathlib/Algebra/Order/Monoid/Lemmas.lean

@@ -940,6 +940,16 @@ theorem mul_eq_one_iff' [CovariantClass α α (· * ·) (· ≤ ·)]
     -- `fun ⟨ha', hb'⟩ => by rw [ha', hb', mul_one]`,
     -- had its `to_additive`-ization fail due to some bug
 
+@[to_additive] lemma mul_le_mul_iff_of_ge [CovariantClass α α (· * ·) (· ≤ ·)]
+  [CovariantClass α α (swap (· * ·)) (· ≤ ·)] [CovariantClass α α (· * ·) (· < ·)]
+  [CovariantClass α α (swap (· * ·)) (· < ·)] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) :
+  a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂ := by
+  refine' ⟨fun h ↦ _, by rintro ⟨rfl, rfl⟩; rfl⟩
+  simp only [eq_iff_le_not_lt, ha, hb, true_and]
+  refine' ⟨fun ha ↦ h.not_lt _, fun hb ↦ h.not_lt _⟩
+  { exact mul_lt_mul_of_lt_of_le ha hb }
+  { exact mul_lt_mul_of_le_of_lt ha hb }
+
 section Left
 
 variable [CovariantClass α α (· * ·) (· ≤ ·)] {a b : α}