From 110036c4dcafd6b55c84aecfb79ee0b989555630 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Thu, 28 Jan 2016 17:21:28 -0500 Subject: [PATCH] feat(library/algebra/ordered_field): add missing theorems --- library/algebra/ordered_field.lean | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean index b7f4fae5e..5874fbee9 100644 --- a/library/algebra/ordered_field.lean +++ b/library/algebra/ordered_field.lean @@ -121,6 +121,12 @@ section linear_ordered_field theorem mul_lt_of_gt_div_of_neg (Hc : c < 0) (H : a > b / c) : a * c < b := !div_mul_cancel (ne_of_lt Hc) ▸ mul_lt_mul_of_neg_right H Hc + theorem div_lt_of_mul_lt_of_pos (Hc : c > 0) (H : b < a * c) : b / c < a := + calc + a = a * c * (1 / c) : !mul_mul_div (ne_of_gt Hc) + ... > b * (1 / c) : mul_lt_mul_of_pos_right H (one_div_pos_of_pos Hc) + ... = b / c : div_eq_mul_one_div + theorem div_lt_of_mul_gt_of_neg (Hc : c < 0) (H : a * c < b) : b / c < a := calc a = a * c * (1 / c) : !mul_mul_div (ne_of_lt Hc) @@ -463,6 +469,21 @@ section discrete_linear_ordered_field (assume H', absurd H (not_le_of_gt (lt_of_one_div_lt_one_div_of_neg Hb H'))) + theorem one_div_le_of_one_div_le_of_pos (Ha : a > 0) (H : 1 / a ≤ b) : 1 / b ≤ a := + begin + rewrite -(one_div_one_div a), + apply one_div_le_one_div_of_le, + apply one_div_pos_of_pos, + repeat assumption + end + + theorem one_div_le_of_one_div_le_of_neg (Ha : b < 0) (H : 1 / a ≤ b) : 1 / b ≤ a := + begin + rewrite -(one_div_one_div a), + apply one_div_le_one_div_of_le_of_neg, + repeat assumption + end + theorem one_lt_one_div (H1 : 0 < a) (H2 : a < 1) : 1 < 1 / a := one_div_one ▸ one_div_lt_one_div_of_lt H1 H2