From 670ac6ae1908f3056b2d3f178f71a470f7cbe3d6 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Tue, 13 Oct 2015 16:14:59 -0400 Subject: [PATCH] fix(real/order): remove sorry --- library/data/real/order.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/library/data/real/order.lean b/library/data/real/order.lean index aede21c5e..6b220f495 100644 --- a/library/data/real/order.lean +++ b/library/data/real/order.lean @@ -872,18 +872,17 @@ theorem le_of_const_le_const {a b : ℚ} (H : s_le (const a) (const b)) : a ≤ end theorem nat_inv_lt_rat {a : ℚ} (H : a > 0) : ∃ n : ℕ+, n⁻¹ < a := - /-begin + begin existsi (pceil (1 / (a / (2)))), apply lt_of_le_of_lt, rotate 1, apply div_two_lt_of_pos H, rewrite -(one_div_one_div (a / (1 + 1))), apply pceil_helper, - rewrite one_div_one_div, apply pnat.le.refl, apply one_div_pos_of_pos, apply div_pos_of_pos_of_pos H dec_trivial - end-/sorry + end theorem const_lt_const_of_lt {a b : ℚ} (H : a < b) : s_lt (const a) (const b) :=