From 82950e1c5280cd7414e63ff607643b867776cb25 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Tue, 23 Jun 2015 16:47:26 +1000 Subject: [PATCH] chore(library/algebra/ordered_field): remove redundant line in calc --- library/algebra/ordered_field.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean index 3309b1c64..cbe88de1b 100644 --- a/library/algebra/ordered_field.lean +++ b/library/algebra/ordered_field.lean @@ -71,8 +71,7 @@ section linear_ordered_field iff.intro (assume H : 1 < a / b, calc - b = b : refl - ... < b * (a / b) : lt_mul_of_gt_one_right Hb H + b < b * (a / b) : lt_mul_of_gt_one_right Hb H ... = a : mul_div_cancel' Hb') (assume H : b < a, have Hbinv : 1 / b > 0, from div_pos_of_pos Hb, calc