From 0df87bae24e208b631ad495024074882f47dd9a9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Aug 2014 17:58:03 -0700 Subject: [PATCH] chore(library/standard/data/nat/div): remove TODO Signed-off-by: Leonardo de Moura --- library/standard/data/nat/div.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/library/standard/data/nat/div.lean b/library/standard/data/nat/div.lean index 001f59de5..6dff9128e 100644 --- a/library/standard/data/nat/div.lean +++ b/library/standard/data/nat/div.lean @@ -663,9 +663,7 @@ have aux : ∀m, P m n, from aux m theorem gcd_succ (m n : ℕ) : gcd m (succ n) = gcd (succ n) (m mod succ n) := --- TODO: note, fails if "succ n" is not given explicitly --- remember that if_neg needs to infer "decidable" for n ~= 0 -trans (gcd_def _ (succ n)) (if_neg (succ_ne_zero n) _ _) +trans (gcd_def _ _) (if_neg (succ_ne_zero n) _ _) theorem gcd_one (n : ℕ) : gcd n 1 = 1 := sorry -- (by simp) (gcd_succ n 0)