fix: patch for std4#198

Mathlib/Algebra/EuclideanDomain/Instances.lean

@@ -33,7 +33,7 @@ instance Int.euclideanDomain : EuclideanDomain ℤ :=
       not_lt_of_ge <| by
         rw [← mul_one a.natAbs, Int.natAbs_mul]
         rw [← Int.natAbs_pos] at b0
-        exact Nat.mul_le_mul_of_nonneg_left b0 }
+        exact Nat.mul_le_mul_left _ b0 }
 
 -- see Note [lower instance priority]
 instance (priority := 100) Field.toEuclideanDomain {K : Type*} [Field K] : EuclideanDomain K :=

Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean

@@ -42,7 +42,8 @@ def stepBound (n : ℕ) : ℕ :=
   n * 4 ^ n
 #align szemeredi_regularity.step_bound SzemerediRegularity.stepBound
 
-theorem le_stepBound : id ≤ stepBound := fun n => Nat.le_mul_of_pos_right <| pow_pos (by norm_num) n
+theorem le_stepBound : id ≤ stepBound := fun n =>
+  Nat.le_mul_of_pos_right _ <| pow_pos (by norm_num) n
 #align szemeredi_regularity.le_step_bound SzemerediRegularity.le_stepBound
 
 theorem stepBound_mono : Monotone stepBound := fun a b h =>
@@ -215,7 +216,7 @@ noncomputable def bound : ℕ :=
 #align szemeredi_regularity.bound SzemerediRegularity.bound
 
 theorem initialBound_le_bound : initialBound ε l ≤ bound ε l :=
-  (id_le_iterate_of_id_le le_stepBound _ _).trans <| Nat.le_mul_of_pos_right <| by positivity
+  (id_le_iterate_of_id_le le_stepBound _ _).trans <| Nat.le_mul_of_pos_right _ <| by positivity
 #align szemeredi_regularity.initial_bound_le_bound SzemerediRegularity.initialBound_le_bound
 
 theorem le_bound : l ≤ bound ε l :=

Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean

@@ -68,10 +68,11 @@ theorem equitabilise_aux (hs : a * m + b * (m + 1) = s.card) :
       ite (0 < a) (a - 1) a * m + ite (0 < a) b (b - 1) * (m + 1) = s.card - n := by
     rw [hn, ← hs]
     split_ifs with h <;> rw [tsub_mul, one_mul]
-    · refine' ⟨m_pos, le_succ _, le_add_right (le_mul_of_pos_left ‹0 < a›), _⟩
-      rw [tsub_add_eq_add_tsub (le_mul_of_pos_left h)]
-    · refine' ⟨succ_pos', le_rfl, le_add_left (le_mul_of_pos_left <| hab.resolve_left ‹¬0 < a›), _⟩
-      rw [← add_tsub_assoc_of_le (le_mul_of_pos_left <| hab.resolve_left ‹¬0 < a›)]
+    · refine' ⟨m_pos, le_succ _, le_add_right (Nat.le_mul_of_pos_left _ ‹0 < a›), _⟩
+      rw [tsub_add_eq_add_tsub (Nat.le_mul_of_pos_left _ h)]
+    · refine' ⟨succ_pos', le_rfl,
+        le_add_left (Nat.le_mul_of_pos_left _ <| hab.resolve_left ‹¬0 < a›), _⟩
+      rw [← add_tsub_assoc_of_le (Nat.le_mul_of_pos_left _ <| hab.resolve_left ‹¬0 < a›)]
   /- We will call the inductive hypothesis on a partition of `s \ t` for a carefully chosen `t ⊆ s`.
     To decide which, however, we must distinguish the case where all parts of `P` have size `m` (in
     which case we take `t` to be an arbitrary subset of `s` of size `n`) from the case where at

Mathlib/Data/FP/Basic.lean

@@ -97,7 +97,7 @@ theorem Float.Zero.valid : ValidFinite emin 0 :=
       ring_nf
       rw [mul_comm]
       assumption
-    le_trans C.precMax (Nat.le_mul_of_pos_left (by decide)),
+    le_trans C.precMax (Nat.le_mul_of_pos_left _ two_pos),
     by (rw [max_eq_right]; simp [sub_eq_add_neg])⟩
 #align fp.float.zero.valid FP.Float.Zero.valid
 

Mathlib/Data/List/Rotate.lean

@@ -445,7 +445,7 @@ theorem IsRotated.symm (h : l ~r l') : l' ~r l := by
   · exists 0
   · use (hd :: tl).length * n - n
     rw [rotate_rotate, add_tsub_cancel_of_le, rotate_length_mul]
-    exact Nat.le_mul_of_pos_left (by simp)
+    exact Nat.le_mul_of_pos_left _ (by simp)
 #align list.is_rotated.symm List.IsRotated.symm
 
 theorem isRotated_comm : l ~r l' ↔ l' ~r l :=

Mathlib/Data/Nat/Basic.lean

@@ -380,8 +380,8 @@ lemma one_lt_mul_iff : 1 < m * n ↔ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n) := by
     · simp at h
     · exact (Nat.mul_le_mul h'.1 h'.2).not_lt h
   · obtain hm | hn := h.2.2
-    · exact Nat.mul_lt_mul hm h.2.1 Nat.zero_lt_one
-    · exact Nat.mul_lt_mul' h.1 hn h.1
+    · exact Nat.mul_lt_mul_of_lt_of_le hm h.2.1 h.2.1
+    · exact Nat.mul_lt_mul_of_le_of_lt h.1 hn h.1
 
 /-!
 ### Recursion and induction principles

Mathlib/Data/Nat/Choose/Central.lean

@@ -40,7 +40,7 @@ theorem centralBinom_eq_two_mul_choose (n : ℕ) : centralBinom n = (2 * n).choo
 #align nat.central_binom_eq_two_mul_choose Nat.centralBinom_eq_two_mul_choose
 
 theorem centralBinom_pos (n : ℕ) : 0 < centralBinom n :=
-  choose_pos (Nat.le_mul_of_pos_left zero_lt_two)
+  choose_pos (Nat.le_mul_of_pos_left _ zero_lt_two)
 #align nat.central_binom_pos Nat.centralBinom_pos
 
 theorem centralBinom_ne_zero (n : ℕ) : centralBinom n ≠ 0 :=
@@ -62,7 +62,7 @@ theorem choose_le_centralBinom (r n : ℕ) : choose (2 * n) r ≤ centralBinom n
 
 theorem two_le_centralBinom (n : ℕ) (n_pos : 0 < n) : 2 ≤ centralBinom n :=
   calc
-    2 ≤ 2 * n := le_mul_of_pos_right n_pos
+    2 ≤ 2 * n := Nat.le_mul_of_pos_right _ n_pos
     _ = (2 * n).choose 1 := (choose_one_right (2 * n)).symm
     _ ≤ centralBinom n := choose_le_centralBinom 1 n
 #align nat.two_le_central_binom Nat.two_le_centralBinom
@@ -112,7 +112,7 @@ theorem four_pow_le_two_mul_self_mul_centralBinom :
     calc
       4 ^ (n+4) ≤ (n+4) * centralBinom (n+4) := (four_pow_lt_mul_centralBinom _ le_add_self).le
       _ ≤ 2 * (n+4) * centralBinom (n+4) := by
-        rw [mul_assoc]; refine' le_mul_of_pos_left zero_lt_two
+        rw [mul_assoc]; refine' Nat.le_mul_of_pos_left _ zero_lt_two
 #align nat.four_pow_le_two_mul_self_mul_central_binom Nat.four_pow_le_two_mul_self_mul_centralBinom
 
 theorem two_dvd_centralBinom_succ (n : ℕ) : 2 ∣ centralBinom (n + 1) := by

Mathlib/Data/Nat/Factorial/Basic.lean

@@ -274,11 +274,15 @@ theorem pow_succ_le_ascFactorial (n : ℕ) : ∀ k : ℕ, (n + 1) ^ k ≤ n.ascF
     exact Nat.mul_le_mul (Nat.add_le_add_right le_self_add _) (pow_succ_le_ascFactorial _ k)
 #align nat.pow_succ_le_asc_factorial Nat.pow_succ_le_ascFactorial
 
+theorem ascFactorial_pos (n k : ℕ) : 0 < n.ascFactorial k :=
+  (pow_pos (succ_pos n) k).trans_le (pow_succ_le_ascFactorial n k)
+#align nat.asc_factorial_pos Nat.ascFactorial_pos
+
 theorem pow_lt_ascFactorial' (n k : ℕ) : (n + 1) ^ (k + 2) < n.ascFactorial (k + 2) := by
   rw [pow_succ, ascFactorial, mul_comm]
   exact
-    Nat.mul_lt_mul (Nat.add_lt_add_right (Nat.lt_add_of_pos_right succ_pos') 1)
-      (pow_succ_le_ascFactorial n _) (pow_pos succ_pos' _)
+    Nat.mul_lt_mul_of_lt_of_le (Nat.add_lt_add_right (Nat.lt_add_of_pos_right succ_pos') 1)
+      (pow_succ_le_ascFactorial n _) (ascFactorial_pos _ _)
 #align nat.pow_lt_asc_factorial' Nat.pow_lt_ascFactorial'
 
 theorem pow_lt_ascFactorial (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1) ^ k < n.ascFactorial k
@@ -292,8 +296,8 @@ theorem ascFactorial_le_pow_add (n : ℕ) : ∀ k : ℕ, n.ascFactorial k ≤ (n
   | k + 1 => by
     rw [ascFactorial_succ, pow_succ, ← add_assoc, mul_comm _ (succ (n + k))]
     exact
-      Nat.mul_le_mul_of_nonneg_left
-        ((ascFactorial_le_pow_add _ k).trans (Nat.pow_le_pow_left (le_succ _) _))
+      Nat.mul_le_mul_left _
+        ((ascFactorial_le_pow_add _ k).trans (Nat.pow_le_pow_of_le_left (le_succ _) _))
 #align nat.asc_factorial_le_pow_add Nat.ascFactorial_le_pow_add
 
 theorem ascFactorial_lt_pow_add (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → n.ascFactorial k < (n + k) ^ k
@@ -306,10 +310,6 @@ theorem ascFactorial_lt_pow_add (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → n.ascFact
       Nat.pow_lt_pow_left (lt_add_one _) k.succ_ne_zero) (succ_pos _)
 #align nat.asc_factorial_lt_pow_add Nat.ascFactorial_lt_pow_add
 
-theorem ascFactorial_pos (n k : ℕ) : 0 < n.ascFactorial k :=
-  (pow_pos (succ_pos n) k).trans_le (pow_succ_le_ascFactorial n k)
-#align nat.asc_factorial_pos Nat.ascFactorial_pos
-
 end AscFactorial
 
 section DescFactorial
@@ -401,8 +401,8 @@ theorem pow_sub_le_descFactorial (n : ℕ) : ∀ k : ℕ, (n + 1 - k) ^ k ≤ n.
   | 0 => by rw [descFactorial_zero, pow_zero]
   | k + 1 => by
     rw [descFactorial_succ, pow_succ, succ_sub_succ, mul_comm]
-    apply Nat.mul_le_mul_of_nonneg_left
-    exact   (le_trans (Nat.pow_le_pow_left (tsub_le_tsub_right (le_succ _) _) k)
+    apply Nat.mul_le_mul_left
+    exact   (le_trans (Nat.pow_le_pow_of_le_left (tsub_le_tsub_right (le_succ _) _) k)
           (pow_sub_le_descFactorial n k))
 #align nat.pow_sub_le_desc_factorial Nat.pow_sub_le_descFactorial
 
@@ -443,7 +443,7 @@ theorem descFactorial_lt_pow {n : ℕ} (hn : 1 ≤ n) : ∀ {k : ℕ}, 2 ≤ k 
   | 1 => by intro; contradiction
   | k + 2 => fun _ => by
     rw [descFactorial_succ, pow_succ', mul_comm, mul_comm n]
-    exact Nat.mul_lt_mul' (descFactorial_le_pow _ _) (tsub_lt_self hn k.zero_lt_succ)
+    exact Nat.mul_lt_mul_of_le_of_lt (descFactorial_le_pow _ _) (tsub_lt_self hn k.zero_lt_succ)
       (pow_pos (Nat.lt_of_succ_le hn) _)
 #align nat.desc_factorial_lt_pow Nat.descFactorial_lt_pow
 

Mathlib/Data/Nat/Factorial/DoubleFactorial.lean

@@ -57,7 +57,7 @@ theorem factorial_eq_mul_doubleFactorial : ∀ n : ℕ, (n + 1)! = (n + 1)‼ *
 lemma doubleFactorial_le_factorial : ∀ n, n‼ ≤ n !
   | 0 => le_rfl
   | n + 1 => by
-    rw [factorial_eq_mul_doubleFactorial]; exact le_mul_of_pos_right n.doubleFactorial_pos
+    rw [factorial_eq_mul_doubleFactorial]; exact Nat.le_mul_of_pos_right _ n.doubleFactorial_pos
 
 theorem doubleFactorial_two_mul : ∀ n : ℕ, (2 * n)‼ = 2 ^ n * n !
   | 0 => rfl

Mathlib/Data/Nat/Fib/Basic.lean

@@ -193,7 +193,7 @@ theorem fib_two_mul_add_two (n : ℕ) :
   rw [fib_add_two, fib_two_mul, fib_two_mul_add_one]
   -- porting note: A bunch of issues similar to [this zulip thread](https://github.com/leanprover-community/mathlib4/pull/1576) with `zify`
   have : fib n ≤ 2 * fib (n + 1) :=
-    le_trans (fib_le_fib_succ) (mul_comm 2 _ ▸ le_mul_of_pos_right two_pos)
+    le_trans (fib_le_fib_succ) (mul_comm 2 _ ▸ Nat.le_mul_of_pos_right _ two_pos)
   zify [this]
   ring
 

Mathlib/Data/Nat/Order/Basic.lean

@@ -288,18 +288,10 @@ theorem le_mul_self : ∀ n : ℕ, n ≤ n * n
   | n + 1 => by simp
 #align nat.le_mul_self Nat.le_mul_self
 
-theorem le_mul_of_pos_left (h : 0 < n) : m ≤ n * m := by
-  conv =>
-    lhs
-    rw [← one_mul m]
-  exact mul_le_mul_of_nonneg_right h.nat_succ_le (zero_le _)
+-- Moved to Std
 #align nat.le_mul_of_pos_left Nat.le_mul_of_pos_left
 
-theorem le_mul_of_pos_right (h : 0 < n) : m ≤ m * n := by
-  conv =>
-    lhs
-    rw [← mul_one m]
-  exact mul_le_mul_of_nonneg_left h.nat_succ_le (zero_le _)
+-- Moved to Std
 #align nat.le_mul_of_pos_right Nat.le_mul_of_pos_right
 
 theorem mul_self_inj : m * m = n * n ↔ m = n :=
@@ -476,7 +468,7 @@ theorem not_dvd_of_pos_of_lt (h1 : 0 < n) (h2 : n < m) : ¬m ∣ n := by
   rintro ⟨k, rfl⟩
   rcases Nat.eq_zero_or_pos k with (rfl | hk)
   · exact lt_irrefl 0 h1
-  · exact not_lt.2 (le_mul_of_pos_right hk) h2
+  · exact not_lt.2 (Nat.le_mul_of_pos_right _ hk) h2
 #align nat.not_dvd_of_pos_of_lt Nat.not_dvd_of_pos_of_lt
 
 /-- If `m` and `n` are equal mod `k`, `m - n` is zero mod `k`. -/

Mathlib/Data/Nat/Sqrt.lean

@@ -57,7 +57,7 @@ private theorem sqrt_isSqrt (n : ℕ) : IsSqrt n (sqrt n) := by
     rw [lt_add_one_iff, add_assoc, ← mul_two]
     refine le_trans (div_add_mod' (n + 2) 2).ge ?_
     rw [add_comm, add_le_add_iff_right, add_mod_right]
-    simp only [zero_lt_two, add_div_right, succ_mul_succ_eq]
+    simp only [zero_lt_two, add_div_right, succ_mul_succ]
     refine le_trans (b := 1) ?_ ?_
     · exact (lt_succ.1 $ mod_lt n zero_lt_two)
     · simp only [le_add_iff_nonneg_left]; exact zero_le _

Mathlib/Data/ZMod/Basic.lean

@@ -1161,7 +1161,7 @@ theorem natAbs_min_of_le_div_two (n : ℕ) (x y : ℤ) (he : (x : ZMod n) = y) (
   rw [← add_le_add_iff_right x.natAbs]
   refine' le_trans (le_trans ((add_le_add_iff_left _).2 hl) _) (Int.natAbs_sub_le _ _)
   rw [add_sub_cancel, Int.natAbs_mul, Int.natAbs_ofNat]
-  refine' le_trans _ (Nat.le_mul_of_pos_right <| Int.natAbs_pos.2 hm)
+  refine' le_trans _ (Nat.le_mul_of_pos_right _ <| Int.natAbs_pos.2 hm)
   rw [← mul_two]; apply Nat.div_mul_le_self
 #align zmod.nat_abs_min_of_le_div_two ZMod.natAbs_min_of_le_div_two
 

Mathlib/FieldTheory/SeparableDegree.lean

@@ -583,7 +583,7 @@ theorem finSepDegree_eq_finrank_of_isSeparable [IsSeparable F E] :
     rw [H L h] at hd
     by_cases hd' : finSepDegree L E = 0
     · rw [← hd, hd', mul_zero]
-    linarith only [h', hd, Nat.le_mul_of_pos_right (m := finrank F L) (Nat.pos_of_ne_zero hd')]
+    linarith only [h', hd, Nat.le_mul_of_pos_right (finrank F L) (Nat.pos_of_ne_zero hd')]
   rw [← finSepDegree_top F, ← finrank_top F E]
   refine induction_on_adjoin (fun K : IntermediateField F E ↦ finSepDegree F K = finrank F K)
     (by simp_rw [finSepDegree_bot, IntermediateField.finrank_bot]) (fun L x h ↦ ?_) ⊤
@@ -603,7 +603,7 @@ theorem finSepDegree_eq_finrank_iff [FiniteDimensional F E] :
     have halg := IsAlgebraic.of_finite F x
     refine (finSepDegree_adjoin_simple_eq_finrank_iff F E x halg).1 <| le_antisymm
       (finSepDegree_adjoin_simple_le_finrank F E x halg) <| le_of_not_lt fun h ↦ ?_
-    have := Nat.mul_lt_mul h (finSepDegree_le_finrank F⟮x⟯ E) Fin.size_pos'
+    have := Nat.mul_lt_mul_of_lt_of_le' h (finSepDegree_le_finrank F⟮x⟯ E) Fin.size_pos'
     rw [finSepDegree_mul_finSepDegree_of_isAlgebraic F F⟮x⟯ E (Algebra.IsAlgebraic.of_finite _ E),
       FiniteDimensional.finrank_mul_finrank F F⟮x⟯ E] at this
     linarith only [heq, this]⟩, fun _ ↦ finSepDegree_eq_finrank_of_isSeparable F E⟩

Mathlib/Init/Data/Nat/Lemmas.lean

@@ -462,7 +462,7 @@ Many lemmas are proven more generally in mathlib `algebra/order/sub` -/
 
 #align nat.mul_self_sub_mul_self_eq Nat.mul_self_sub_mul_self_eq
 
-#align nat.succ_mul_succ_eq Nat.succ_mul_succ_eq
+#align nat.succ_mul_succ_eq Nat.succ_mul_succ
 
 /-! min -/
 

Mathlib/NumberTheory/Divisors.lean

@@ -126,7 +126,8 @@ theorem mem_divisorsAntidiagonal {x : ℕ × ℕ} :
     simp only [succ_le_of_lt (Nat.pos_of_ne_zero h.1), succ_le_of_lt (Nat.pos_of_ne_zero h.2),
       true_and_iff]
     exact
-      ⟨le_mul_of_pos_right (Nat.pos_of_ne_zero h.2), le_mul_of_pos_left (Nat.pos_of_ne_zero h.1)⟩
+      ⟨Nat.le_mul_of_pos_right _ (Nat.pos_of_ne_zero h.2),
+        Nat.le_mul_of_pos_left _ (Nat.pos_of_ne_zero h.1)⟩
 #align nat.mem_divisors_antidiagonal Nat.mem_divisorsAntidiagonal
 
 -- Porting note: Redundant binder annotation update

Mathlib/NumberTheory/FermatPsp.lean

@@ -318,7 +318,7 @@ private theorem psp_from_prime_gt_p {b : ℕ} (b_ge_two : 2 ≤ b) {p : ℕ} (p_
   suffices h : p * b ^ 2 < (b ^ 2) ^ (p - 1) * b ^ 2
   · apply gt_of_ge_of_gt
     · exact tsub_le_tsub_left (one_le_of_lt p_gt_two) ((b ^ 2) ^ (p - 1) * b ^ 2)
-    · have : p ≤ p * b ^ 2 := Nat.le_mul_of_pos_right (show 0 < b ^ 2 by nlinarith)
+    · have : p ≤ p * b ^ 2 := Nat.le_mul_of_pos_right _ (show 0 < b ^ 2 by nlinarith)
       exact tsub_lt_tsub_right_of_le this h
   suffices h : p < (b ^ 2) ^ (p - 1)
   · have : 4 ≤ b ^ 2 := by nlinarith
@@ -352,7 +352,7 @@ theorem exists_infinite_pseudoprimes {b : ℕ} (h : 1 ≤ b) (m : ℕ) :
     have h₄ : 0 < b * (b ^ 2 - 1) := mul_pos h₁ h₃
     have h₅ : b * (b ^ 2 - 1) < p := by linarith
     have h₆ : ¬p ∣ b * (b ^ 2 - 1) := Nat.not_dvd_of_pos_of_lt h₄ h₅
-    have h₇ : b ≤ b * (b ^ 2 - 1) := Nat.le_mul_of_pos_right h₃
+    have h₇ : b ≤ b * (b ^ 2 - 1) := Nat.le_mul_of_pos_right _ h₃
     have h₈ : 2 ≤ b * (b ^ 2 - 1) := le_trans b_ge_two h₇
     have h₉ : 2 < p := gt_of_gt_of_ge h₅ h₈
     have h₁₀ := psp_from_prime_gt_p b_ge_two hp₂ h₉

Mathlib/Tactic/NormNum/LegendreSymbol.lean

@@ -78,8 +78,7 @@ theorem jacobiSymNat.zero_left (b : ℕ) (hb : Nat.beq (b / 2) 0 = false) : jaco
   · calc
       1 < 2 * 1       := by decide
       _ ≤ 2 * (b / 2) :=
-        Nat.mul_le_mul_of_nonneg_left
-          (Nat.succ_le.mpr (Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb)))
+        Nat.mul_le_mul_left _ (Nat.succ_le.mpr (Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb)))
       _ ≤ b           := Nat.mul_div_le b 2
 #align norm_num.jacobi_sym_nat.zero_left_even Mathlib.Meta.NormNum.jacobiSymNat.zero_left
 #align norm_num.jacobi_sym_nat.zero_left_odd Mathlib.Meta.NormNum.jacobiSymNat.zero_left

test/apply_rules.lean

@@ -7,17 +7,17 @@ open Nat
 example {a b c d e : Nat} (h1 : a ≤ b) (h2 : c ≤ d) (h3 : 0 ≤ e) :
     a + c * e + a + c + 0 ≤ b + d * e + b + d + e :=
   Nat.add_le_add (Nat.add_le_add (Nat.add_le_add
-    (Nat.add_le_add h1 (Nat.mul_le_mul_of_nonneg_right h2)) h1) h2) h3
+    (Nat.add_le_add h1 (Nat.mul_le_mul_right _ h2)) h1) h2) h3
 
 example {a b c d e : Nat} (h1 : a ≤ b) (h2 : c ≤ d) (h3 : 0 ≤ e) :
     a + c * e + a + c + 0 ≤ b + d * e + b + d + e := by
-  apply_rules [Nat.add_le_add, Nat.mul_le_mul_of_nonneg_right]
+  apply_rules [Nat.add_le_add, Nat.mul_le_mul_right]
 
 -- Check that when we supply an iteration bound,
 -- `apply_rules` works up to that bound and returns the remaining goals.
 example {a b c d e : Nat} (h1 : a ≤ b) (h2 : c ≤ d) (h3 : 0 ≤ e) :
     a + c * e + a + c + 0 ≤ b + d * e + b + d + e := by
-  apply_rules (config := {maxDepth := 9}) [Nat.add_le_add, Nat.mul_le_mul_of_nonneg_right]
+  apply_rules (config := {maxDepth := 9}) [Nat.add_le_add, Nat.mul_le_mul_right]
   guard_target = 0 ≤ e
   assumption