From 0eec984485d1ea29c636ba96b199ea02f0fa3f7a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 12 Oct 2015 16:56:11 -0700 Subject: [PATCH] fix(library/data/equiv): minor adjustment --- library/data/equiv.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/data/equiv.lean b/library/data/equiv.lean index 509d0ac7e..ef53dede1 100644 --- a/library/data/equiv.lean +++ b/library/data/equiv.lean @@ -277,7 +277,7 @@ mk (λ s, match s with inl n := 2*n | inr n := 2*n+1 end) rewrite [if_neg h], esimp, cases n, {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)))]} end))