diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index 46f783dd60..98940afd9c 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -411,13 +411,16 @@ theorem not_eq_zero_of_pos (h : 0 < a) : a ≠ 0 := by
   contradiction
   apply Nat.noConfusion
 
-theorem add_sub_self (a b : Nat) : (a + b) - a = b := by
+theorem add_sub_self_left (a b : Nat) : (a + b) - a = b := by
   induction a with
   | zero => simp
   | succ a ih =>
     rw [Nat.succ_add, Nat.succ_sub_succ]
     apply ih
 
+theorem add_sub_self_right (a b : Nat) : (a + b) - b = a := by
+  rw [Nat.add_comm]; apply add_sub_self_left
+
 theorem sub_le_succ_sub (a i : Nat) : a - i ≤ a.succ - i := by
   cases i with
   | zero => apply Nat.le_of_lt; apply Nat.lt_succ_self
@@ -428,7 +431,7 @@ theorem zero_lt_sub_of_lt (h : i < a) : 0 < a - i := by
   | zero => contradiction
   | succ a ih =>
     match Nat.eq_or_lt_of_le h with
-    | Or.inl h => injection h with h; subst h; rw [←Nat.add_one, Nat.add_sub_self]; decide
+    | Or.inl h => injection h with h; subst h; rw [←Nat.add_one, Nat.add_sub_self_left]; decide
     | Or.inr h =>
       have : 0 < a - i := ih (Nat.lt_of_succ_lt_succ h)
       exact Nat.lt_of_lt_of_le this (Nat.sub_le_succ_sub _ _)
diff --git a/tests/lean/run/860.lean b/tests/lean/run/860.lean
index 8883934f63..5b16f7d0b0 100644
--- a/tests/lean/run/860.lean
+++ b/tests/lean/run/860.lean
@@ -1,19 +1,12 @@
 def evenq (n: Nat) : Bool := Nat.mod n 2 = 0
 
-theorem Nat.add_sub_self (a b : Nat) : (a + b) - b = a := by
-  induction b with
-  | zero => rfl
-  | succ n ih =>
-    show (a + n).succ - n.succ = a
-    rw [Nat.succ_sub_succ, ih]
-
 private theorem pack_loop_terminates : (n : Nat) → n / 2 < n.succ
   | 0   => by decide
   | 1   => by decide
   | n+2 => by
     rw [Nat.div_eq]
     split
-    . rw [Nat.add_sub_self]
+    . rw [Nat.add_sub_self_right]
       have := pack_loop_terminates n
       calc n/2 + 1 < Nat.succ n + 1   := Nat.add_le_add_right this 1
              _     < Nat.succ (n + 2) := Nat.succ_lt_succ (Nat.succ_lt_succ (Nat.lt_succ_self _))