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

fix(library/data/equiv): minor adjustment

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-12 16:56:11 -07:00
parent d1e111fd6c
commit 0eec984485
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/equiv.lean
View file

@ -277,7 +277,7 @@ mk (λ s, match s with inl n := 2*n | inr n := 2*n+1 end)
rewrite [if_neg h], esimp, rewrite [if_neg h], esimp,
cases n, cases n,
{exact absurd even_zero h}, {exact absurd even_zero h},
{rewrite [-add_one, add_sub_cancel, {rewrite [-(add_one a), add_sub_cancel,
mul_div_cancel' (dvd_of_even (even_of_odd_succ (odd_of_not_even h)))]} mul_div_cancel' (dvd_of_even (even_of_odd_succ (odd_of_not_even h)))]}
end)) end))