chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use ZeroLEOneClass

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -249,7 +249,7 @@ lemma short_needle_inter_eq (h : l ≤ d) (θ : ℝ) :
     Set.Icc (-θ.sin * l / 2) (θ.sin * l / 2) := by
   rw [Set.Icc_inter_Icc, inf_eq_min, sup_eq_max, max_div_div_right zero_le_two,
     min_div_div_right zero_le_two, neg_mul, max_neg_neg, mul_comm,
-    min_eq_right (mul_le_of_le_of_le_one_of_nonneg h θ.sin_le_one hl.le)]
+    min_eq_right ((mul_le_of_le_one_right hl.le θ.sin_le_one).trans h)]
 
 include hd hBₘ hB hl in
 /--

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

@@ -130,11 +130,6 @@ instance (priority := 100) LinearOrderedCommGroupWithZero.toMulPosStrictMono :
     MulPosStrictMono α where
   elim a b c hbc := by by_contra! h; exact hbc.not_le <| (mul_le_mul_right a.2).1 h
 
-/-- Alias of `one_le_mul'` for unification. -/
-@[deprecated one_le_mul (since := "2024-08-21")]
-theorem one_le_mul₀ (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b :=
-  one_le_mul ha hb
-
 @[deprecated mul_le_mul_right (since := "2024-08-21")]
 theorem le_of_le_mul_right (h : c ≠ 0) (hab : a * c ≤ b * c) : a ≤ b :=
   (mul_le_mul_right (zero_lt_iff.2 h)).1 hab