feat: Add mul_inv and inv_mul versions of div_le_one_of_le (#10597

)

These are exactly `div_le_one_of_le` with `a / b` replaced by `a * b⁻¹` and `b⁻¹ * a`.

They come up frequently because some tactics produce inverses as normal forms over division.  The iff versions with `0 < b` already exist as `mul_inv_le_one_iff` and `inv_mul_le_one_iff`; the point of these is to have a weaker nonnegativity assumption on `b`.

Mathlib/Algebra/Order/Field/Basic.lean

@@ -243,6 +243,12 @@ theorem div_le_one_of_le (h : a ≤ b) (hb : 0 ≤ b) : a / b ≤ 1 :=
   div_le_of_nonneg_of_le_mul hb zero_le_one <| by rwa [one_mul]
 #align div_le_one_of_le div_le_one_of_le
 
+lemma mul_inv_le_one_of_le (h : a ≤ b) (hb : 0 ≤ b) : a * b⁻¹ ≤ 1 := by
+  simpa only [← div_eq_mul_inv] using div_le_one_of_le h hb
+
+lemma inv_mul_le_one_of_le (h : a ≤ b) (hb : 0 ≤ b) : b⁻¹ * a ≤ 1 := by
+  simpa only [← div_eq_inv_mul] using div_le_one_of_le h hb
+
 /-!
 ### Bi-implications of inequalities using inversions
 -/