From 2e5284add799bc6e87aa351e6eb56192dc2cb935 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Wed, 23 Aug 2017 16:13:28 -0400 Subject: [PATCH] fix(library/init/algebra/ordered_field): remove unused argument from div_two_lt_of_pos --- library/init/algebra/ordered_field.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/algebra/ordered_field.lean b/library/init/algebra/ordered_field.lean index a6b95a4d98..7b6c69beff 100644 --- a/library/init/algebra/ordered_field.lean +++ b/library/init/algebra/ordered_field.lean @@ -319,7 +319,7 @@ begin apply le_mul_of_div_le hc h end -lemma div_two_lt_of_pos {a b : α} (h : a > 0) : a / 2 < a := +lemma div_two_lt_of_pos {a : α} (h : a > 0) : a / 2 < a := suffices a / (1 + 1) < a, begin unfold bit0, assumption end, have ha : a / 2 > 0, from div_pos_of_pos_of_pos h (add_pos zero_lt_one zero_lt_one), calc