diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index dbab8cd9ef..f37423ded2 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -599,22 +599,22 @@ protected theorem sub_self : ∀ (n : ℕ), n - n = 0
 
 /- TODO(Leo): remove the following ematch annotations as soon as we have
    arithmetic theory in the smt_stactic -/
-@[ematch]
+@[ematch_lhs]
 protected theorem add_sub_add_right : ∀ (n k m : ℕ), (n + k) - (m + k) = n - m
 | n 0        m := by rw [add_zero, add_zero]
 | n (succ k) m := by rw [add_succ, add_succ, succ_sub_succ, add_sub_add_right n k m]
 
-@[ematch]
+@[ematch_lhs]
 protected theorem add_sub_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m :=
 by rw [add_comm k n, add_comm k m, nat.add_sub_add_right]
 
-@[ematch]
+@[ematch_lhs]
 protected theorem add_sub_cancel (n m : ℕ) : n + m - m = n :=
 suffices n + m - (0 + m) = n, from
   by rwa [zero_add] at this,
 by rw [nat.add_sub_add_right, nat.sub_zero]
 
-@[ematch]
+@[ematch_lhs]
 protected theorem add_sub_cancel_left (n m : ℕ) : n + m - n = m :=
 show n + m - (n + 0) = m, from
 by rw [nat.add_sub_add_left, nat.sub_zero]
diff --git a/tests/lean/run/nat_sub_ematch.lean b/tests/lean/run/nat_sub_ematch.lean
new file mode 100644
index 0000000000..41a794ac20
--- /dev/null
+++ b/tests/lean/run/nat_sub_ematch.lean
@@ -0,0 +1,13 @@
+set_option trace.smt.ematch true
+
+example (a b c d : nat) (f : nat → nat) : f d = a + b → f d - a + c = c + b :=
+begin [smt]
+  intros,
+  eblast
+end
+
+example (a b c d : nat) (f : nat → nat) : f d = a + b → f d - (a + c) = b - c :=
+begin [smt]
+  intros,
+  eblast
+end