From d9528ffad8f60e8e18bb7e67ef66358e9a044277 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 21 Jan 2017 03:11:59 -0800 Subject: [PATCH] chore(library/init/data/nat/lemmas): add comment --- library/init/data/nat/lemmas.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index 8d79bb8aa8..dbab8cd9ef 100644 --- a/library/init/data/nat/lemmas.lean +++ b/library/init/data/nat/lemmas.lean @@ -597,6 +597,8 @@ protected theorem sub_self : ∀ (n : ℕ), n - n = 0 | 0 := by rw nat.sub_zero | (succ n) := by rw [succ_sub_succ, sub_self n] +/- TODO(Leo): remove the following ematch annotations as soon as we have + arithmetic theory in the smt_stactic -/ @[ematch] protected theorem add_sub_add_right : ∀ (n k m : ℕ), (n + k) - (m + k) = n - m | n 0 m := by rw [add_zero, add_zero]