From e01b155b2eecb2da12d3c070c6445f66ef88c5c2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 31 Aug 2015 16:53:11 -1000 Subject: [PATCH] refactor(library/data/int/basic): cleanup proof Proof was abusing the higher-order unifier --- library/data/int/basic.lean | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 74737951d..1c10c3bce 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -533,7 +533,14 @@ end migrate_algebra /- additional properties -/ theorem of_nat_sub {m n : ℕ} (H : m ≥ n) : m - n = sub m n := -(sub_eq_of_eq_add (!congr_arg (nat.sub_add_cancel H)⁻¹))⁻¹ +assert m - n + n = m, from nat.sub_add_cancel H, +begin + symmetry, + apply sub_eq_of_eq_add, + rewrite [-of_nat_add, this] +end + +-- (sub_eq_of_eq_add (!congr_arg (nat.sub_add_cancel H)⁻¹))⁻¹ theorem neg_succ_of_nat_eq' (m : ℕ) : -[1+ m] = -m - 1 := by rewrite [neg_succ_of_nat_eq, of_nat_add, neg_add]