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

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

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-22 15:10:50 -07:00
parent a1d200e1c6
commit bd41b6ea13
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/data/rat/basic.lean
View file

@ -242,7 +242,8 @@ have H : smul (denom a) (mul a (add b c)) (denom_pos a) =
have T : ∀ {x y z w : ℤ}, x*y*z*w=y*z*x*w, from
λx y z w, (!int.mul.assoc ⬝ !int.mul.comm) ▸ rfl,
exact !congr_arg2 T T,
exact !mul.left_comm ▸ !int.mul.assoc⁻¹
rewrite [mul.left_comm (denom a) (denom b) (denom c)],
rewrite int.mul.assoc
end,
equiv.symm (H ▸ smul_equiv (denom_pos a))