michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/data/int/basic): cleanup proof

Browse source 
Proof was abusing the higher-order unifier
This commit is contained in:
Leonardo de Moura 2015-08-31 16:53:11 -10:00
parent 2b1d2c21ad
commit e01b155b2e
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/data/int/basic.lean
View file

@ -533,7 +533,14 @@ end migrate_algebra
/- additional properties -/ /- additional properties -/
theorem of_nat_sub {m n : ℕ} (H : m ≥ n) : m - n = sub m n := 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 := theorem neg_succ_of_nat_eq' (m : ℕ) : -[1+ m] = -m - 1 :=
by rewrite [neg_succ_of_nat_eq, of_nat_add, neg_add] by rewrite [neg_succ_of_nat_eq, of_nat_add, neg_add]