feat(*): use ordered_sub instead of nat.sub lemmas (#9855)

* For all `nat.sub` lemmas in core, prefer to use the `has_ordered_sub` version.
* Most lemmas have an identical version for `has_ordered_sub`. In some cases we only have the symmetric version.
* Make arguments to `tsub_add_eq_tsub_tsub` and `tsub_add_eq_tsub_tsub_swap` explicit
* Rename `add_tsub_add_right_eq_tsub -> add_tsub_add_eq_tsub_right` (for consistency with the `_left` version)
* Rename `sub_mul' -> tsub_mul` and `mul_sub' -> mul_tsub` (these were forgotten in #9793)
* Many of the fixes are to fix the identification of `n < m` and `n.succ \le m`.
* Add projection notation `h.nat_succ_le` for `nat.succ_le_of_lt h`.

archive/100-theorems-list/83_friendship_graphs.lean

@@ -274,7 +274,7 @@ begin
   { cases fintype.card V with n,
     { exact zero_le _, },
     { have : n = 0,
-      { rw [nat.succ_sub_succ_eq_sub, nat.sub_zero] at h,
+      { rw [nat.succ_sub_succ_eq_sub, tsub_zero] at h,
         linarith },
       subst n, } },
   use classical.arbitrary V,

archive/imo/imo1977_q6.lean

@@ -25,7 +25,7 @@ begin
     { intros n hk,
       apply nat.succ_le_of_lt,
       calc k ≤ f (f (n - 1)) : h_ind _ (h_ind (n - 1) (le_tsub_of_add_le_right hk))
-         ... < f n           : nat.sub_add_cancel
+         ... < f n           : tsub_add_cancel_of_le
         (le_trans (nat.succ_le_succ (nat.zero_le _)) hk) ▸ h _ } },
   have hf : ∀ n, n ≤ f n := λ n, h' n n rfl.le,
   have hf_mono : strict_mono f := strict_mono_nat_of_lt_succ (λ _, lt_of_le_of_lt (hf _) (h _)),

archive/imo/imo1981_q3.lean

@@ -130,7 +130,7 @@ begin
     { have h7 : nat_predicate N (n - m) m, from h2.reduction h4,
       obtain ⟨k : ℕ, hnm : n - m = fib k, rfl : m = fib (k+1)⟩ := h1 m h6 (n - m) h7,
       use [k + 1, rfl],
-      rw [fib_succ_succ, ← hnm, nat.sub_add_cancel h3] } }
+      rw [fib_succ_succ, ← hnm, tsub_add_cancel_of_le h3] } }
 end
 
 end nat_predicate

archive/miu_language/decision_suf.lean

@@ -181,7 +181,7 @@ end arithmetic
 lemma repeat_pow_minus_append  {m : ℕ} : M :: repeat I (2^m - 1) ++ [I] = M::(repeat I (2^m)) :=
 begin
   change [I] with repeat I 1,
-  rw [cons_append, ←repeat_add, nat.sub_add_cancel (one_le_pow' m 1)],
+  rw [cons_append, ←repeat_add, tsub_add_cancel_of_le (one_le_pow' m 1)],
 end
 
 /--
@@ -204,7 +204,7 @@ begin
   { apply der_cons_repeat_I_repeat_U_append_of_der_cons_repeat_I_append c ((2^m-c)/3) h,
     convert hw₂, -- now we must show `c + 3 * ((2 ^ m - c) / 3) = 2 ^ m`
     rw nat.mul_div_cancel',
-    { exact nat.add_sub_of_le hm.1 },
+    { exact add_tsub_cancel_of_le hm.1 },
     { exact (modeq_iff_dvd' hm.1).mp hm.2.symm } },
   rw [append_assoc, ←repeat_add _ _] at hw₃,
   cases add_mod2 ((2^m-c)/3) with t ht,
@@ -228,7 +228,7 @@ begin
   { apply der_cons_repeat_I_repeat_U_append_of_der_cons_repeat_I_append c ((2^m-c)/3) h,
     convert hw₂, -- now we must show `c + 3 * ((2 ^ m - c) / 3) = 2 ^ m`
     rw nat.mul_div_cancel',
-    { exact nat.add_sub_of_le hm.1 },
+    { exact add_tsub_cancel_of_le hm.1 },
     { exact (modeq_iff_dvd' hm.1).mp hm.2.symm } },
   rw [append_assoc, ←repeat_add _ _] at hw₃,
   cases add_mod2 ((2^m-c)/3) with t ht,

archive/oxford_invariants/2021summer/week3_p1.lean

@@ -97,7 +97,7 @@ begin
     { rw [nat.cast_one, finset.sum_range_one, div_self],
       exact (mul_pos (a_pos 0 (nat.zero_le _)) (a_pos 1 (nat.zero_lt_succ _))).ne' },
     -- Check the divisibility condition
-    { rw [mul_one, nat.sub_self],
+    { rw [mul_one, tsub_self],
       exact dvd_zero _ } },
   /- Induction step
   `b` is the value of the previous sum as a natural, `hb` is the proof that it is indeed the value,
@@ -133,7 +133,7 @@ begin
             (a_pos _ $ nat.le_succ _).ne', mul_comm],
         end },
   -- Check the divisibility condition
-  { rw [nat.mul_sub_left_distrib, ← mul_assoc, nat.mul_div_cancel' ha, add_mul,
-      nat.mul_div_cancel' han, add_tsub_tsub_cancel ha₀, nat.add_sub_cancel],
+  { rw [mul_tsub, ← mul_assoc, nat.mul_div_cancel' ha, add_mul,
+      nat.mul_div_cancel' han, add_tsub_tsub_cancel ha₀, add_tsub_cancel_right],
     exact dvd_mul_right _ _ }
 end

counterexamples/canonically_ordered_comm_semiring_two_mul.lean

@@ -231,7 +231,7 @@ begin
     { exact ⟨(0 : L), (add_zero _).symm⟩ },
     { refine ⟨⟨⟨bn - an, b2 + a2⟩, _⟩, _⟩,
       { rw [ne.def, prod.mk.inj_iff, not_and_distrib],
-        exact or.inl (ne_of_gt (nat.sub_pos_of_lt h)) },
+        exact or.inl (ne_of_gt (tsub_pos_of_lt h)) },
       { congr,
         { exact (add_tsub_cancel_of_le h.le).symm },
         { change b2 = a2 + (b2 + a2),

src/algebra/big_operators/basic.lean

@@ -928,10 +928,10 @@ when the function we are summing is monotone.
 lemma sum_range_sub_of_monotone {f : ℕ → ℕ} (h : monotone f) (n : ℕ) :
   ∑ i in range n, (f (i+1) - f i) = f n - f 0 :=
 begin
-  refine sum_range_induction _ _ (nat.sub_self _) (λ n, _) _,
+  refine sum_range_induction _ _ (tsub_self _) (λ n, _) _,
   have h₁ : f n ≤ f (n+1) := h (nat.le_succ _),
   have h₂ : f 0 ≤ f n := h (nat.zero_le _),
-  rw [←nat.sub_add_comm h₂, add_tsub_cancel_of_le h₁],
+  rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁],
 end
 
 @[simp] lemma prod_const (b : β) : (∏ x in s, b) = b ^ s.card :=

src/algebra/big_operators/intervals.lean

@@ -90,9 +90,9 @@ lemma prod_Ico_eq_prod_range (f : ℕ → β) (m n : ℕ) :
   (∏ k in Ico m n, f k) = (∏ k in range (n - m), f (m + k)) :=
 begin
   by_cases h : m ≤ n,
-  { rw [←nat.Ico_zero_eq_range, prod_Ico_add, zero_add, nat.sub_add_cancel h] },
+  { rw [←nat.Ico_zero_eq_range, prod_Ico_add, zero_add, tsub_add_cancel_of_le h] },
   { replace h : n ≤ m :=  le_of_not_ge h,
-     rw [Ico_eq_empty_of_le h, nat.sub_eq_zero_of_le h, range_zero, prod_empty, prod_empty] }
+     rw [Ico_eq_empty_of_le h, tsub_eq_zero_iff_le.mpr h, range_zero, prod_empty, prod_empty] }
 end
 
 lemma prod_Ico_reflect (f : ℕ → β) (k : ℕ) {m n : ℕ} (h : m ≤ n + 1) :
@@ -106,8 +106,8 @@ begin
     refine (prod_image _).symm,
     simp only [mem_Ico],
     rintros i ⟨ki, im⟩ j ⟨kj, jm⟩ Hij,
-    rw [← nat.sub_sub_self (this _ im), Hij, nat.sub_sub_self (this _ jm)] },
-  { simp [Ico_eq_empty_of_le, nat.sub_le_sub_left, hkm] }
+    rw [← tsub_tsub_cancel_of_le (this _ im), Hij, tsub_tsub_cancel_of_le (this _ jm)] },
+  { simp [Ico_eq_empty_of_le, tsub_le_tsub_left, hkm] }
 end
 
 lemma sum_Ico_reflect {δ : Type*} [add_comm_monoid δ] (f : ℕ → δ) (k : ℕ) {m n : ℕ}
@@ -120,7 +120,7 @@ lemma prod_range_reflect (f : ℕ → β) (n : ℕ) :
 begin
   cases n,
   { simp },
-  { simp only [←nat.Ico_zero_eq_range, nat.succ_sub_succ_eq_sub, nat.sub_zero],
+  { simp only [←nat.Ico_zero_eq_range, nat.succ_sub_succ_eq_sub, tsub_zero],
     rw prod_Ico_reflect _ _ le_rfl,
     simp }
 end

src/algebra/char_p/basic.lean

@@ -117,10 +117,10 @@ theorem add_pow_char_of_commute [semiring R] {p : ℕ} [fact p.prime]
   [char_p R p] (x y : R) (h : commute x y) :
   (x + y)^p = x^p + y^p :=
 begin
-  rw [commute.add_pow h, finset.sum_range_succ_comm, nat.sub_self, pow_zero, nat.choose_self],
+  rw [commute.add_pow h, finset.sum_range_succ_comm, tsub_self, pow_zero, nat.choose_self],
   rw [nat.cast_one, mul_one, mul_one], congr' 1,
   convert finset.sum_eq_single 0 _ _,
-  { simp only [mul_one, one_mul, nat.choose_zero_right, nat.sub_zero, nat.cast_one, pow_zero] },
+  { simp only [mul_one, one_mul, nat.choose_zero_right, tsub_zero, nat.cast_one, pow_zero] },
   { intros b h1 h2,
     suffices : (p.choose b : R) = 0, { rw this, simp },
     rw char_p.cast_eq_zero_iff R p,

src/algebra/continued_fractions/terminated_stable.lean

@@ -40,8 +40,8 @@ begin
       have stable_step : g.continuants_aux (m - 1 + 2) = g.continuants_aux (m - 1 + 1), from
         continuants_aux_stable_step_of_terminated this,
       have one_le_m : 1 ≤ m, from nat.one_le_of_lt succ_n_le_m,
-      have : m - 1 + 2 = m + 2 - 1, from (nat.sub_add_comm one_le_m).symm,
-      have : m - 1 + 1 = m + 1 - 1, from (nat.sub_add_comm one_le_m).symm,
+      have : m - 1 + 2 = m + 2 - 1, from tsub_add_eq_add_tsub one_le_m,
+      have : m - 1 + 1 = m + 1 - 1, from tsub_add_eq_add_tsub one_le_m,
       simpa [*] using stable_step },
     exact (eq.trans this IH) }
 end

src/algebra/geom_sum.lean

@@ -82,7 +82,7 @@ begin
   refine sum_congr rfl (λ j j_in, _),
   rw [mem_range, nat.lt_iff_add_one_le] at j_in,
   congr,
-  apply nat.sub_sub_self,
+  apply tsub_tsub_cancel_of_le,
   exact le_tsub_of_add_le_right j_in
 end
 
@@ -100,19 +100,19 @@ begin
   { rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero] },
   { have f_last : f (n + 1) n = (x + y) ^ n :=
      by { dsimp [f],
-          rw [nat.sub_sub, nat.add_comm, nat.sub_self, pow_zero, mul_one] },
+          rw [← tsub_add_eq_tsub_tsub, nat.add_comm, tsub_self, pow_zero, mul_one] },
     have f_succ : ∀ i, i ∈ range n → f (n + 1) i = y * f n i :=
       λ i hi, by {
         dsimp [f],
         have : commute y ((x + y) ^ i) :=
          (h.symm.add_right (commute.refl y)).pow_right i,
         rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ y (n - 1 - i)],
         congr' 2,
-        rw [nat.add_sub_cancel, nat.sub_sub, add_comm 1 i],
-        have : i + 1 + (n - (i + 1)) = n := nat.add_sub_of_le (mem_range.mp hi),
+        rw [add_tsub_cancel_right, ← tsub_add_eq_tsub_tsub, add_comm 1 i],
+        have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi),
         rw [add_comm (i + 1)] at this,
-        rw [← this, nat.add_sub_cancel, add_comm i 1, ← add_assoc,
-            nat.add_sub_cancel] },
+        rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc,
+            add_tsub_cancel_right] },
     rw [pow_succ (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc],
     rw (((commute.refl x).add_right h).pow_right n).eq,
     congr' 1,
@@ -221,27 +221,27 @@ begin
       congr,
       rw [mem_range, nat.lt_iff_add_one_le, add_comm] at j_in,
       have h' : n - m + (m - (1 + j)) = n - (1 + j) := tsub_add_tsub_cancel hmn j_in,
-      rw [nat.sub_sub m, h', nat.sub_sub] },
+      rw [← tsub_add_eq_tsub_tsub m, h', ← tsub_add_eq_tsub_tsub] },
   rw this,
   simp_rw pow_mul_comm y (n-m) _,
   simp_rw ← mul_assoc,
   rw [← sum_mul, ← geom_sum₂_def, mul_sub, h.mul_geom_sum₂, ← mul_assoc,
-    h.mul_geom_sum₂, sub_mul, ← pow_add, nat.add_sub_of_le hmn,
+    h.mul_geom_sum₂, sub_mul, ← pow_add, add_tsub_cancel_of_le hmn,
     sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ n)],
 end
 
 protected theorem commute.geom_sum₂_succ_eq {α : Type u} [ring α] {x y : α}
   (h : commute x y) {n : ℕ} :
   geom_sum₂ x y (n + 1) = x ^ n + y * (geom_sum₂ x y n) :=
 begin
-  simp_rw [geom_sum₂, mul_sum, sum_range_succ_comm, nat.add_succ_sub_one, add_zero, nat.sub_self,
+  simp_rw [geom_sum₂, mul_sum, sum_range_succ_comm, nat.add_succ_sub_one, add_zero, tsub_self,
     pow_zero, mul_one, add_right_inj, ←mul_assoc, (h.symm.pow_right _).eq, mul_assoc, ←pow_succ],
   refine sum_congr rfl (λ i hi, _),
   suffices : n - 1 - i + 1 = n - i, { rw this },
   cases n,
   { exact absurd (list.mem_range.mp hi) i.not_lt_zero },
   { rw [tsub_add_eq_add_tsub (nat.le_pred_of_lt (list.mem_range.mp hi)),
-        nat.sub_add_cancel (nat.succ_le_iff.mpr n.succ_pos)] },
+        tsub_add_cancel_of_le (nat.succ_le_iff.mpr n.succ_pos)] },
 end
 
 theorem geom_sum₂_succ_eq {α : Type u} [comm_ring α] (x y : α)  {n : ℕ} :
@@ -329,20 +329,20 @@ calc
   (b - 1) * (∑ i in range n.succ, a/b^i)
       = ∑ i in range n, a/b^(i + 1) * b + a * b
         - (∑ i in range n, a/b^i + a/b^n)
-      : by rw [nat.mul_sub_right_distrib, mul_comm, sum_mul, one_mul, sum_range_succ',
+      : by rw [tsub_mul, mul_comm, sum_mul, one_mul, sum_range_succ',
           sum_range_succ, pow_zero, nat.div_one]
   ... ≤ ∑ i in range n, a/b^i + a * b - (∑ i in range n, a/b^i + a/b^n)
       : begin
-        refine nat.sub_le_sub_right (add_le_add_right (sum_le_sum $ λ i _, _) _) _,
+        refine tsub_le_tsub_right (add_le_add_right (sum_le_sum $ λ i _, _) _) _,
         rw [pow_succ', ←nat.div_div_eq_div_mul],
         exact nat.div_mul_le_self _ _,
       end
-  ... = a * b - a/b^n : nat.add_sub_add_left _ _ _
+  ... = a * b - a/b^n : add_tsub_add_eq_tsub_left _ _ _
 
 lemma nat.geom_sum_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) :
   ∑ i in range n, a/b^i ≤ a * b/(b - 1) :=
 begin
-  refine (nat.le_div_iff_mul_le _ _ $ nat.sub_pos_of_lt hb).2 _,
+  refine (nat.le_div_iff_mul_le _ _ $ tsub_pos_of_lt hb).2 _,
   cases n,
   { rw [sum_range_zero, zero_mul],
     exact nat.zero_le _ },
@@ -368,5 +368,5 @@ begin
     ... = (a * 1 + a * (b - 1))/(b - 1)
         : by rw [←mul_add, add_tsub_cancel_of_le (one_le_two.trans hb)]
     ... = a + a/(b - 1)
-        : by rw [mul_one, nat.add_mul_div_right _ _ (nat.sub_pos_of_lt hb), add_comm]
+        : by rw [mul_one, nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]
 end

src/algebra/group_power/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
-import algebra.order.ring
+import data.nat.basic
 import tactic.monotonicity.basic
 import group_theory.group_action.defs
 
@@ -172,11 +172,11 @@ by rw [nat.mul_comm, pow_mul]
 
 @[to_additive nsmul_add_sub_nsmul]
 theorem pow_mul_pow_sub (a : M) {m n : ℕ} (h : m ≤ n) : a ^ m * a ^ (n - m) = a ^ n :=
-by rw [←pow_add, nat.add_comm, nat.sub_add_cancel h]
+by rw [←pow_add, nat.add_comm, tsub_add_cancel_of_le h]
 
 @[to_additive sub_nsmul_nsmul_add]
 theorem pow_sub_mul_pow (a : M) {m n : ℕ} (h : m ≤ n) : a ^ (n - m) * a ^ m = a ^ n :=
-by rw [←pow_add, nat.sub_add_cancel h]
+by rw [←pow_add, tsub_add_cancel_of_le h]
 
 @[to_additive bit0_nsmul]
 theorem pow_bit0 (a : M) (n : ℕ) : a ^ bit0 n = a^n * a^n := pow_add _ _ _
@@ -303,7 +303,7 @@ end
 
 @[to_additive nsmul_sub] -- rename to sub_nsmul?
 theorem pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a^(m - n) = a^m * (a^n)⁻¹ :=
-have h1 : m - n + n = m, from nat.sub_add_cancel h,
+have h1 : m - n + n = m, from tsub_add_cancel_of_le h,
 have h2 : a^(m - n) * a^n = a^m, by rw [←pow_add, h1],
 eq_mul_inv_of_mul_eq h2
 
@@ -376,7 +376,7 @@ end
 
 lemma pow_eq_zero_of_le [monoid_with_zero M] {x : M} {n m : ℕ}
   (hn : n ≤ m) (hx : x^n = 0) : x^m = 0 :=
-by rw [← nat.sub_add_cancel hn, pow_add, hx, mul_zero]
+by rw [← tsub_add_cancel_of_le hn, pow_add, hx, mul_zero]
 
 namespace ring_hom
 
@@ -408,7 +408,7 @@ lemma mul_neg_one_pow_eq_zero_iff [ring R] {n : ℕ} {r : R} : r * (-1)^n = 0 
 by rcases neg_one_pow_eq_or R n; simp [h]
 
 lemma pow_dvd_pow [monoid R] (a : R) {m n : ℕ} (h : m ≤ n) :
-  a ^ m ∣ a ^ n := ⟨a ^ (n - m), by rw [← pow_add, nat.add_comm, nat.sub_add_cancel h]⟩
+  a ^ m ∣ a ^ n := ⟨a ^ (n - m), by rw [← pow_add, nat.add_comm, tsub_add_cancel_of_le h]⟩
 
 theorem pow_dvd_pow_of_dvd [comm_monoid R] {a b : R} (h : a ∣ b) : ∀ n : ℕ, a ^ n ∣ b ^ n
 | 0     := by rw [pow_zero, pow_zero]

src/algebra/group_power/lemmas.lean

@@ -73,7 +73,7 @@ def invertible_of_pow_eq_one (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : 0 < n) :
 begin
   apply invertible_of_pow_succ_eq_one x (n - 1),
   convert hx,
-  exact nat.sub_add_cancel (nat.succ_le_of_lt hn),
+  exact tsub_add_cancel_of_le (nat.succ_le_of_lt hn),
 end
 
 lemma is_unit_of_pow_eq_one (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : 0 < n) :

src/algebra/group_power/order.lean

@@ -156,7 +156,7 @@ theorem pow_lt_pow_of_lt_left {x y : R} {n : ℕ} (Hxy : x < y) (Hxpos : 0 ≤ x
   x ^ n < y ^ n :=
 begin
   cases lt_or_eq_of_le Hxpos,
-  { rw ←nat.sub_add_cancel Hnpos,
+  { rw ← tsub_add_cancel_of_le (nat.succ_le_of_lt Hnpos),
     induction (n - 1), { simpa only [pow_one] },
     rw [pow_add, pow_add, nat.succ_eq_add_one, pow_one, pow_one],
     apply mul_lt_mul ih (le_of_lt Hxy) h (le_of_lt (pow_pos (lt_trans h Hxy) _)) },

src/algebra/group_with_zero/power.lean

@@ -44,7 +44,7 @@ begin
 end
 
 theorem pow_sub₀ (a : G₀) {m n : ℕ} (ha : a ≠ 0) (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ :=
-have h1 : m - n + n = m, from nat.sub_add_cancel h,
+have h1 : m - n + n = m, from tsub_add_cancel_of_le h,
 have h2 : a ^ (m - n) * a ^ n = a ^ m, by rw [←pow_add, h1],
 by simpa only [div_eq_mul_inv] using eq_div_of_mul_eq (pow_ne_zero _ ha) h2
 

src/algebra/linear_recurrence.lean

@@ -65,7 +65,7 @@ def mk_sol (init : fin E.order → α) : ℕ → α
   ∑ k : fin E.order,
     have n - E.order + k < n :=
     begin
-      rw [add_comm, ← nat.add_sub_assoc (not_lt.mp h), tsub_lt_iff_left],
+      rw [add_comm, ← add_tsub_assoc_of_le (not_lt.mp h), tsub_lt_iff_left],
       { exact add_lt_add_right k.is_lt n },
       { convert add_le_add (zero_le (k : ℕ)) (not_lt.mp h),
         simp only [zero_add] }
@@ -88,12 +88,12 @@ lemma eq_mk_of_is_sol_of_eq_init {u : ℕ → α} {init : fin E.order → α}
 | n := if h' : n < E.order
   then by rw mk_sol; simp only [h', dif_pos]; exact_mod_cast heq ⟨n, h'⟩
   else begin
-    rw [mk_sol, ← nat.sub_add_cancel (le_of_not_lt h'), h (n-E.order)],
+    rw [mk_sol, ← tsub_add_cancel_of_le (le_of_not_lt h'), h (n-E.order)],
     simp [h'],
     congr' with k,
     exact have wf : n - E.order + k < n :=
       begin
-        rw [add_comm, ← nat.add_sub_assoc (not_lt.mp h'), tsub_lt_iff_left],
+        rw [add_comm, ← add_tsub_assoc_of_le (not_lt.mp h'), tsub_lt_iff_left],
         { exact add_lt_add_right k.is_lt n },
         { convert add_le_add (zero_le (k : ℕ)) (not_lt.mp h'),
           simp only [zero_add] }

src/algebra/order/ring.lean

@@ -1412,26 +1412,26 @@ variables [has_sub α] [has_ordered_sub α]
 variables [is_total α (≤)]
 
 namespace add_le_cancellable
-protected lemma mul_sub (h : add_le_cancellable (a * c)) :
+protected lemma mul_tsub (h : add_le_cancellable (a * c)) :
   a * (b - c) = a * b - a * c :=
 begin
   cases total_of (≤) b c with hbc hcb,
   { rw [tsub_eq_zero_iff_le.2 hbc, mul_zero, tsub_eq_zero_iff_le.2 (mul_le_mul_left' hbc a)] },
   { apply h.eq_tsub_of_add_eq, rw [← mul_add, tsub_add_cancel_of_le hcb] }
 end
 
-protected lemma sub_mul (h : add_le_cancellable (b * c)) : (a - b) * c = a * c - b * c :=
-by { simp only [mul_comm _ c] at *, exact h.mul_sub }
+protected lemma tsub_mul (h : add_le_cancellable (b * c)) : (a - b) * c = a * c - b * c :=
+by { simp only [mul_comm _ c] at *, exact h.mul_tsub }
 
 end add_le_cancellable
 
 variables [contravariant_class α α (+) (≤)]
 
-lemma mul_sub' (a b c : α) : a * (b - c) = a * b - a * c :=
-contravariant.add_le_cancellable.mul_sub
+lemma mul_tsub (a b c : α) : a * (b - c) = a * b - a * c :=
+contravariant.add_le_cancellable.mul_tsub
 
-lemma sub_mul' (a b c : α) : (a - b) * c = a * c - b * c :=
-contravariant.add_le_cancellable.sub_mul
+lemma tsub_mul (a b c : α) : (a - b) * c = a * c - b * c :=
+contravariant.add_le_cancellable.tsub_mul
 
 end sub