diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index 23aeecd902..a6dd924f16 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -562,6 +562,19 @@ theorem le_add_of_sub_le {a b c : Nat} (h : a - b ≤ c) : a ≤ c + b := by
     have hd := Nat.eq_add_of_sub_eq (Nat.le_trans hge (Nat.le_add_left ..)) hd
     rw [Nat.add_comm, hd]
 
+@[simp] protected theorem zero_sub (n : Nat) : 0 - n = 0 := by
+  induction n with
+  | zero => rfl
+  | succ n ih => simp [ih, Nat.sub_succ]
+
+protected theorem sub_self_add (n m : Nat) : n - (n + m) = 0 := by
+  show (n + 0) - (n + m) = 0
+  rw [Nat.add_sub_add_left, Nat.zero_sub]
+
+protected theorem sub_eq_zero_of_le {n m : Nat} (h : n ≤ m) : n - m = 0 := by
+  match le.dest h with
+  | ⟨k, hk⟩ => rw [← hk, Nat.sub_self_add]
+
 theorem sub_le_of_le_add {a b c : Nat} (h : a ≤ c + b) : a - b ≤ c := by
   match le.dest h, Nat.le_total a b with
   | _, Or.inl hle =>
@@ -594,19 +607,6 @@ theorem le_sub_of_add_le {a b c : Nat} (h : a + b ≤ c) : a ≤ c - b := by
 @[simp] protected theorem pred_succ (n : Nat) : pred n.succ = n :=
   rfl
 
-@[simp] protected theorem zero_sub (n : Nat) : 0 - n = 0 := by
-  induction n with
-  | zero => rfl
-  | succ n ih => simp [ih, Nat.sub_succ]
-
-protected theorem sub_self_add (n m : Nat) : n - (n + m) = 0 := by
-  show (n + 0) - (n + m) = 0
-  rw [Nat.add_sub_add_left, Nat.zero_sub]
-
-protected theorem sub_eq_zero_of_le {n m : Nat} (h : n ≤ m) : n - m = 0 := by
-  match le.dest h with
-  | ⟨k, hk⟩ => rw [← hk, Nat.sub_self_add]
-
 theorem sub.elim {motive : Nat → Prop}
     (x y : Nat)
     (h₁ : y ≤ x → (k : Nat) → x = y + k → motive k)
diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean
index ec368c4752..d447fcdebc 100644
--- a/src/Init/Data/Nat/Linear.lean
+++ b/src/Init/Data/Nat/Linear.lean
@@ -451,7 +451,7 @@ theorem Poly.denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r
             simp [denote_le] at h |-
             have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
             rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]
-            apply Nat.sub_le_of_le_add (Nat.le_trans haux (Nat.le_add_left ..))
+            apply Nat.sub_le_of_le_add
             simp [h]
           . have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk
             apply ih
@@ -484,7 +484,7 @@ theorem Poly.of_denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
           . have ih := ih (h := h); simp [denote_le] at ih ⊢
             have haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hgtk))
             rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux] at ih
-            have := Nat.le_add_of_sub_le (Nat.le_trans haux (Nat.le_add_left ..)) ih
+            have := Nat.le_add_of_sub_le ih
             simp at this
             exact this
           . have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk; subst heqk