fix(library/init/data/nat/lemmas): avoid bad patterns in nat sub ematch lemmas

The attribute [ematch_lhs] instructs Lean to use the left-hand-side of
the conclusion as a pattern.

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]

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