feat(library/algebra/ordered_field): prove more theorems

library/algebra/field.lean

@@ -62,6 +62,8 @@ section division_ring
 
   theorem div_self (H : a ≠ 0) : a / a = 1 := mul_inv_cancel H
 
+  theorem one_div_one : 1 / 1 = 1 := div_self (ne.symm zero_ne_one)
+
   theorem mul_div_assoc : (a * b) / c = a * (b / c) := !mul.assoc
 
   theorem one_div_ne_zero (H : a ≠ 0) : 1 / a ≠ 0 :=

library/algebra/ordered_field.lean

@@ -26,13 +26,9 @@ section linear_ordered_field
   have nhc : -c ≥ 0, from neg_nonneg_of_nonpos Hc,
   have H2 : -(c * b) < -(c * a), from (iff.mp' (neg_lt_neg_iff_lt _ _) H),
   have H3 : (-c) * b < (-c) * a, from (calc
-    (-c) * b = (-1 * c) * b : neg_eq_neg_one_mul
+    (-c) * b = - (c * b)    : neg_mul_eq_neg_mul
-         ... = -1 * (c * b) : mul.assoc
-         ... = - (c * b)    : neg_eq_neg_one_mul
          ... < -(c * a)     : H2
-         ... = -1 * (c * a) : neg_eq_neg_one_mul
+         ... = (-c) * a     : neg_mul_eq_neg_mul
-         ... = (-1 * c) * a : mul.assoc
-         ... = (-c) * a     : neg_eq_neg_one_mul
   ),
   lt_of_mul_lt_mul_left H3 nhc
 
@@ -92,6 +88,12 @@ section linear_ordered_field
        ... ≤ a * (1 / b) : mul_le_mul_of_nonneg_right H (le_of_lt Hbinv)
        ... = a / b       : div_eq_mul_one_div)
 
+  theorem le_of_one_le_div (Hb : b > 0) (H : 1 ≤ a / b) : b ≤ a :=
+    (iff.mp (one_le_div_iff_le Hb)) H
+
+  theorem one_le_div_of_le (Hb : b > 0) (H : b ≤ a) : 1 ≤ a / b :=
+    (iff.mp' (one_le_div_iff_le Hb)) H
+
   theorem one_lt_div_iff_lt (Hb : b > 0) : 1 < a / b ↔ b < a :=
     have Hb' : b ≠ 0, from ne.symm (ne_of_lt Hb),
     iff.intro
@@ -106,6 +108,12 @@ section linear_ordered_field
       ... < a * (1 / b) : mul_lt_mul_of_pos_right H Hbinv
       ... = a / b       : div_eq_mul_one_div)
 
+  theorem lt_of_one_lt_div (Hb : b > 0) (H : 1 < a / b) : b < a :=
+    (iff.mp (one_lt_div_iff_lt Hb)) H
+
+  theorem one_lt_div_of_lt (Hb : b > 0) (H : b < a) : 1 < a / b :=
+    (iff.mp' (one_lt_div_iff_lt Hb)) H
+
 -- why is mul_le_mul under ordered_ring namespace?
   theorem le_of_div_le (H : 0 < a) (Hl : 1 / a ≤ 1 / b) : b ≤ a :=
     have Hb : 0 < b, from pos_of_div_pos (calc
@@ -116,7 +124,7 @@ section linear_ordered_field
       ... = a * (1 / a) :  div_eq_mul_one_div
       ... ≤ a * (1 / b) : ordered_ring.mul_le_mul_of_nonneg_left Hl (le_of_lt H)
       ... = a / b       : div_eq_mul_one_div
-      ), iff.mp (one_le_div_iff_le Hb) H' 
+      ), le_of_one_le_div Hb H' 
       
 
   theorem lt_of_div_lt (H : 0 < a) (Hl : 1 / a < 1 / b) : b < a :=
@@ -128,7 +136,7 @@ section linear_ordered_field
       ... = a * (1 / a) :  div_eq_mul_one_div
       ... < a * (1 / b) : mul_lt_mul_of_pos_left Hl H
       ... = a / b       : div_eq_mul_one_div),
-      iff.mp (one_lt_div_iff_lt Hb) H
+      lt_of_one_lt_div Hb H
 
   theorem le_of_div_le_neg (H : b < 0) (Hl : 1 / a ≤ 1 / b) : b ≤ a :=
     have Ha : a ≠ 0, from ne_of_lt (neg_of_div_neg (calc
@@ -142,7 +150,7 @@ section linear_ordered_field
          ... = 1 / -a    : one_div_neg_eq_neg_one_div Ha,
     le_of_neg_le_neg (le_of_div_le H' Hl'')
 
-  theorem lt_of_div_lt_pos (H : b < 0) (Hl : 1 / a < 1 / b) : b < a :=
+  theorem lt_of_div_lt_neg (H : b < 0) (Hl : 1 / a < 1 / b) : b < a :=
     have H1 : b ≤ a, from le_of_div_le_neg H (le_of_lt Hl),
     have Hn : b ≠ a, from
       (assume Hn' : b = a,
@@ -150,6 +158,72 @@ section linear_ordered_field
       absurd Hl' (ne_of_lt Hl)),
     lt_of_le_of_ne H1 Hn
 
+  theorem div_lt_div_of_lt (Ha : 0 < a) (H : a < b) : 1 / b < 1 / a := 
+    lt_of_not_le
+      (assume H',
+      absurd H (not_lt_of_le (le_of_div_le Ha H'))) 
+
+  theorem div_le_div_of_le (Ha : 0 < a) (H : a ≤ b) : 1 / b ≤ 1 / a := 
+    le_of_not_lt
+      (assume H',
+      absurd H (not_le_of_lt (lt_of_div_lt Ha H')))
+
+  theorem div_lt_div_of_lt_neg (Hb : b < 0) (H : a < b) : 1 / b < 1 / a :=
+    lt_of_not_le
+      (assume H',
+      absurd H (not_lt_of_le (le_of_div_le_neg Hb H')))
+
+  theorem div_le_div_of_le_neg (Hb : b < 0) (H : a ≤ b) : 1 / b ≤ 1 / a :=
+    le_of_not_lt
+      (assume H',
+      absurd H (not_le_of_lt (lt_of_div_lt_neg Hb H')))
+
+  -- belongs in ordered ring?
+  theorem zero_gt_neg_one : -1 < 0 :=
+    neg_zero ▸ (neg_lt_neg zero_lt_one)
+
+  theorem exists_lt : ∃ x, x < a := 
+    have H : a - 1 < a, from add_lt_of_le_of_neg (le.refl _) zero_gt_neg_one,
+    exists.intro _ H
+
+  theorem exists_gt : ∃ x, x > a := 
+    have H : a + 1 > a, from lt_add_of_le_of_pos (le.refl _) zero_lt_one,
+    exists.intro _ H
+
+  theorem one_lt_div (H1 : 0 < a) (H2 : a < 1) : 1 < 1 / a :=
+    one_div_one ▸ div_lt_div_of_lt H1 H2
+
+  theorem one_le_div (H1 : 0 < a) (H2 : a ≤ 1) : 1 ≤ 1 / a :=
+    one_div_one ▸ div_le_div_of_le H1 H2
+
+  theorem neg_one_lt_div_neg (H1 : a < 0) (H2 : -1 < a) : 1 / a < -1 :=
+    one_div_neg_one_eq_neg_one ▸ div_lt_div_of_lt_neg H1 H2
+
+  theorem neg_one_le_div_neg (H1 : a < 0) (H2 : -1 ≤ a) : 1 / a ≤ -1 :=
+    one_div_neg_one_eq_neg_one ▸ div_le_div_of_le_neg H1 H2
+
+  theorem mul_le_of_le_div (Hc : 0 < c) (H : a ≤ b / c) : a * c ≤ b := 
+    div_mul_cancel (ne.symm (ne_of_lt Hc)) ▸ mul_le_mul_of_nonneg_right H (le_of_lt Hc)
+  
+  theorem le_div_of_mul_le (Hc : 0 < c) (H : a * c ≤ b) : a ≤ b / c :=
+    calc
+      a   = a * 1             : mul_one
+      ... = a * (c * (1 / c)) : mul_one_div_cancel (ne.symm (ne_of_lt Hc))
+      ... = a * c * (1 / c)   : mul.assoc
+      ... ≤ b * (1 / c)       : mul_le_mul_of_nonneg_right H (le_of_lt (div_pos_of_pos Hc))
+      ... = b / c             : div_eq_mul_one_div
+
+  theorem mul_lt_of_lt_div (Hc : 0 < c) (H : a < b / c) : a * c < b :=
+    div_mul_cancel (ne.symm (ne_of_lt Hc)) ▸ mul_lt_mul_of_pos_right H Hc
+
+  theorem lt_div_of_mul_lt (Hc : 0 < c) (H : a * c < b) : a < b / c :=
+    calc
+      a   = a * 1             : mul_one
+      ... = a * (c * (1 / c)) : mul_one_div_cancel (ne.symm (ne_of_lt Hc))
+      ... = a * c * (1 / c)   : mul.assoc
+      ... < b * (1 / c)       : mul_lt_mul_of_pos_right H (div_pos_of_pos Hc)
+      ... = b / c             : div_eq_mul_one_div
+
 end linear_ordered_field
 
 structure discrete_linear_ordered_field [class] (A : Type) extends linear_ordered_field A,
@@ -174,7 +248,7 @@ section discrete_linear_ordered_field
 
   definition discrete_linear_ordered_field.to_discrete_field [instance] [reducible] [coercion]
     [s : discrete_linear_ordered_field A] :  discrete_field A :=
-      ⦃ discrete_field, s, decidable_equality := @dec_eq_of_dec_lt A s⦄
+      ⦃ discrete_field, s, decidable_equality := dec_eq_of_dec_lt⦄