feat(library/data/real): prove reals are Cauchy complete

library/data/real/basic.lean

@@ -11,7 +11,7 @@ To do:
  o Rename things and possibly make theorems private
 -/
 
-import algebra.ordered_field data.nat data.rat.order
+import data.nat data.rat.order
 open nat eq eq.ops
 open -[coercions] rat
 ----------------------------------------------------------------------------------------------------
@@ -46,11 +46,11 @@ notation p `≥` q := q ≤ p
 definition lt (p q : pnat) := p~ < q~
 infix `<` := lt
 
-theorem pnat_le_decidable [instance] (p q : pnat) : decidable (p ≤ q) :=
+definition pnat_le_decidable [instance] (p q : pnat) : decidable (p ≤ q) :=
   pnat.rec_on p (λ n H, pnat.rec_on q
     (λ m H2, if Hl : n ≤ m then decidable.inl Hl else decidable.inr Hl))
 
-theorem pnat_lt_decidable [instance] {p q : pnat} : decidable (p < q) :=
+definition pnat_lt_decidable [instance] {p q : pnat} : decidable (p < q) :=
   pnat.rec_on p (λ n H, pnat.rec_on q
     (λ m H2, if Hl : n < m then decidable.inl Hl else decidable.inr Hl))
 
@@ -126,6 +126,8 @@ theorem ge_of_inv_le {p q : ℕ+} (H : p⁻¹ ≤ q⁻¹) : q < p := sorry
 
 theorem padd_halves (p : ℕ+) : (2 * p)⁻¹ + (2 * p)⁻¹ = p⁻¹ := sorry
 
+theorem p_add_fractions (n : ℕ+) : (2 * n)⁻¹ + (2 * 3 * n)⁻¹ + (3 * n)⁻¹ = n⁻¹ := sorry
+
 theorem add_halves_double (m n : ℕ+) :
         m⁻¹ + n⁻¹ = ((2 * m)⁻¹ + (2 * n)⁻¹) + ((2 * m)⁻¹ + (2 * n)⁻¹) :=
   have simp [visible] : ∀ a b : ℚ, (a + a) + (b + b) = (a + b) + (a + b), from sorry,
@@ -150,6 +152,8 @@ theorem pnat_mul_assoc (a b c : ℕ+) : a * b * c = a * (b * c) := sorry
 
 theorem pnat_mul_comm (a b : ℕ+) : a * b = b * a := sorry
 
+theorem pnat_add_assoc (a b c : ℕ+) : a + b + c = a + (b + c) := sorry
+
 theorem s_mul_assoc_lemma_3 (a b n : ℕ+) (p : ℚ) :
         p * ((a * n)⁻¹ + (b * n)⁻¹) = p * (a⁻¹ + b⁻¹) * n⁻¹ := sorry
 

library/data/real/complete.lean

@@ -0,0 +1,484 @@
+/-
+Copyright (c) 2015 Robert Y. Lewis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Robert Y. Lewis
+The real numbers, constructed as equivalence classes of Cauchy sequences of rationals.
+This construction follows Bishop and Bridges (1985).
+
+At this point, we no longer proceed constructively: this file makes heavy use of decidability,
+ excluded middle, and Hilbert choice.
+
+Here, we show that ℝ is complete.
+-/
+ 
+import data.real.basic data.real.order data.real.division data.rat data.nat logic.axioms.classical
+open -[coercions] rat 
+open -[coercions] nat
+open algebra
+open eq.ops
+
+
+local notation 2 := pnat.pos (nat.of_num 2) dec_trivial
+local notation 3 := pnat.pos (nat.of_num 3) dec_trivial
+
+namespace s
+
+theorem nonneg_of_ge_neg_invs (a : ℚ) (H : ∀ n : ℕ+, -n⁻¹ ≤ a) : 0 ≤ a := sorry
+
+theorem ineq_helper (a b c : ℚ) : c ≤ a + b → -a ≤ b - c := sorry
+
+definition const (a : ℚ) : seq := λ n, a
+
+theorem const_reg (a : ℚ) : regular (const a) :=
+  begin
+    intros,
+    rewrite [↑const, sub_self, abs_zero],
+    apply add_invs_nonneg
+  end
+
+definition r_const (a : ℚ) : reg_seq := reg_seq.mk (const a) (const_reg a)
+
+theorem rat_approx_l1 {s : seq} (H : regular s) : 
+        ∀ n : ℕ+, ∃ q : ℚ, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → abs (s m - q) ≤ n⁻¹ :=
+  begin
+    intro n,
+    existsi (s (2 * n)),
+    existsi 2 * n,
+    intro m Hm,
+    apply rat.le.trans,
+    apply H,
+    rewrite -(padd_halves n),
+    apply rat.add_le_add_right,
+    apply inv_ge_of_le Hm
+  end
+
+theorem rat_approx {s : seq} (H : regular s) : 
+        ∀ n : ℕ+, ∃ q : ℚ, s_le (s_abs (sadd s (sneg (const q)))) (const n⁻¹) := 
+  begin
+    intro m,
+    rewrite ↑s_le,
+    apply exists.elim (rat_approx_l1 H m),
+    intro q Hq,
+    apply exists.elim Hq,
+    intro N HN,
+    existsi q,
+    apply nonneg_of_bdd_within,
+    repeat (apply reg_add_reg | apply reg_neg_reg | apply abs_reg_of_reg | apply const_reg
+             | assumption),
+    intro n,
+    existsi N,
+    intro p Hp,
+    rewrite ↑[sadd, sneg, s_abs, const],
+    apply rat.le.trans,
+    rotate 1,
+    apply rat.sub_le_sub_left,
+    apply HN,
+    apply ple.trans,
+    apply Hp,
+    rewrite -*pnat_mul_assoc,
+    apply pnat.mul_le_mul_left,
+    rewrite [sub_self, -neg_zero],
+    apply neg_le_neg,
+    apply rat.le_of_lt,
+    apply inv_pos
+  end
+
+definition r_abs (s : reg_seq) : reg_seq := 
+  reg_seq.mk (s_abs (reg_seq.sq s)) (abs_reg_of_reg (reg_seq.is_reg s))
+
+theorem abs_well_defined {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡ t) :
+        s_abs s ≡ s_abs t := 
+  begin
+    rewrite [↑equiv at *],
+    intro n,
+    rewrite ↑s_abs,
+    apply rat.le.trans,
+    apply abs_abs_sub_abs_le_abs_sub,
+    apply Heq
+  end
+
+theorem r_abs_well_defined {s t : reg_seq} (H : requiv s t) : requiv (r_abs s) (r_abs t) := 
+  abs_well_defined (reg_seq.is_reg s) (reg_seq.is_reg t) H
+
+theorem r_rat_approx (s : reg_seq) :
+        ∀ n : ℕ+, ∃ q : ℚ, r_le (r_abs (radd s (rneg (r_const q)))) (r_const n⁻¹) := 
+  rat_approx (reg_seq.is_reg s)
+
+theorem const_bound {s : seq} (Hs : regular s) (n : ℕ+) : s_le (s_abs (sadd s (sneg (const (s n))))) (const n⁻¹) :=
+  begin
+    rewrite ↑[s_le, nonneg, s_abs, sadd, sneg, const],
+    intro m,
+    apply ineq_helper,
+    apply rat.le.trans,
+    apply Hs,
+    apply rat.add_le_add_right,
+    rewrite -*pnat_mul_assoc,
+    apply inv_ge_of_le,
+    apply pnat.mul_le_mul_left
+  end
+
+theorem abs_const (a : ℚ) : const (abs a) ≡ s_abs (const a) :=
+  begin
+    rewrite [↑s_abs, ↑const],
+    apply equiv.refl
+  end
+
+theorem r_abs_const (a : ℚ) : requiv (r_const (abs a) ) (r_abs (r_const a)) := abs_const a
+
+theorem add_consts (a b : ℚ) : sadd (const a) (const b) ≡ const (a + b) := 
+  begin
+    rewrite [↑sadd, ↑const],
+    apply equiv.refl
+  end
+
+theorem r_add_consts (a b : ℚ) : requiv (r_const a + r_const b) (r_const (a + b)) := add_consts a b
+
+theorem const_le_const_of_le {a b : ℚ} (H : a ≤ b) : s_le (const a) (const b) :=
+  begin
+    rewrite [↑s_le, ↑nonneg],
+    intro n,
+    rewrite [↑sadd, ↑sneg, ↑const],
+    apply rat.le.trans,
+    apply rat.neg_nonpos_of_nonneg,
+    apply rat.le_of_lt,
+    apply inv_pos,
+    apply iff.mp' !rat.sub_nonneg_iff_le,
+    apply H
+  end
+
+theorem le_of_const_le_const {a b : ℚ} (H : s_le (const a) (const b)) : a ≤ b :=
+  begin
+    rewrite [↑s_le at H, ↑nonneg at H, ↑sadd at H, ↑sneg at H, ↑const at H],
+    apply iff.mp !rat.sub_nonneg_iff_le,
+    apply nonneg_of_ge_neg_invs _ H
+  end
+
+theorem r_const_le_const_of_le {a b : ℚ} (H : a ≤ b) : r_le (r_const a) (r_const b) :=
+  const_le_const_of_le H
+
+theorem r_le_of_const_le_const {a b : ℚ} (H : r_le (r_const a) (r_const b)) : a ≤ b :=
+  le_of_const_le_const H
+
+theorem equiv_abs_of_ge_zero {s : seq} (Hs : regular s) (Hz : s_le zero s) : s_abs s ≡ s :=
+  begin 
+    apply eq_of_bdd,
+    apply abs_reg_of_reg Hs,
+    apply Hs,
+    intro j,
+    rewrite ↑s_abs,
+    let Hz' := s_nonneg_of_ge_zero Hs Hz,
+    existsi 2 * j,
+    intro n Hn,
+    apply or.elim (decidable.em (s n ≥ 0)),
+    intro Hpos,
+    rewrite [rat.abs_of_nonneg Hpos, sub_self, abs_zero],
+    apply rat.le_of_lt,
+    apply inv_pos,
+    intro Hneg,
+    let Hneg' := lt_of_not_ge Hneg,
+    have Hsn : -s n - s n > 0, from add_pos (neg_pos_of_neg Hneg') (neg_pos_of_neg Hneg'), 
+    rewrite [rat.abs_of_neg Hneg', rat.abs_of_pos Hsn],
+    apply rat.le.trans,
+    apply rat.add_le_add,
+    repeat (apply rat.neg_le_neg; apply Hz'),
+    rewrite *rat.neg_neg,
+    apply rat.le.trans,
+    apply rat.add_le_add,
+    repeat (apply inv_ge_of_le; apply Hn),
+    rewrite padd_halves,
+    apply rat.le.refl
+  end
+
+theorem equiv_neg_abs_of_le_zero {s : seq} (Hs : regular s) (Hz : s_le s zero) : s_abs s ≡ sneg s :=
+  begin
+    apply eq_of_bdd,
+    apply abs_reg_of_reg Hs,
+    apply reg_neg_reg Hs,
+    intro j,
+    rewrite [↑s_abs, ↑s_le at Hz],
+    have Hz' : nonneg (sneg s), begin
+      apply nonneg_of_nonneg_equiv,
+      rotate 3,
+      apply Hz,
+      rotate 2,
+      apply s_zero_add,
+      repeat (apply Hs | apply zero_is_reg | apply reg_neg_reg | apply reg_add_reg)
+    end,
+    existsi 2 * j,
+    intro n Hn,
+    apply or.elim (decidable.em (s n ≥ 0)),
+    intro Hpos,
+    have Hsn : s n + s n ≥ 0, from add_nonneg Hpos Hpos,
+    rewrite [rat.abs_of_nonneg Hpos, ↑sneg, rat.sub_neg_eq_add, rat.abs_of_nonneg Hsn],
+    rewrite [↑nonneg at Hz', ↑sneg at Hz'],
+    apply rat.le.trans,
+    apply rat.add_le_add,
+    repeat apply (rat.le_of_neg_le_neg !Hz'),
+    apply rat.le.trans,
+    apply rat.add_le_add,
+    repeat (apply inv_ge_of_le; apply Hn),
+    rewrite padd_halves,
+    apply rat.le.refl,
+    intro Hneg,
+    let Hneg' := lt_of_not_ge Hneg,
+    rewrite [rat.abs_of_neg Hneg', ↑sneg, rat.sub_neg_eq_add, rat.neg_add_eq_sub, rat.sub_self,
+                abs_zero], 
+    apply rat.le_of_lt,
+    apply inv_pos
+  end
+
+theorem r_equiv_abs_of_ge_zero {s : reg_seq} (Hz : r_le r_zero s) : requiv (r_abs s) s :=
+  equiv_abs_of_ge_zero (reg_seq.is_reg s) Hz 
+
+theorem r_equiv_neg_abs_of_le_zero {s : reg_seq} (Hz : r_le s r_zero) : requiv (r_abs s) (-s) :=
+  equiv_neg_abs_of_le_zero (reg_seq.is_reg s) Hz
+
+end s
+
+namespace real
+
+theorem rewrite_helper9 (a b c : ℝ) : b - c = (b - a) - (c - a) := sorry
+
+theorem rewrite_helper10 (a b c d : ℝ) : c - d = (c - a) + (a - b) + (b - d) := sorry
+
+theorem r_abs_add_three (a b c : ℝ) : abs (a + b + c) ≤ abs a + abs b + abs c := 
+  begin
+    apply algebra.le.trans,
+    apply algebra.abs_add_le_abs_add_abs,
+    apply algebra.le.trans,
+    apply algebra.add_le_add_right,
+    apply algebra.abs_add_le_abs_add_abs,
+    apply algebra.le.refl
+  end
+
+theorem r_add_le_add_three (a b c d e f : ℝ) (H1 : a ≤ d) (H2 : b ≤ e) (H3 : c ≤ f) :
+        a + b + c ≤ d + e + f := 
+  begin
+    apply algebra.le.trans,
+    apply algebra.add_le_add,
+    apply algebra.add_le_add,
+    repeat assumption,
+    apply algebra.le.refl
+  end
+
+theorem re_add_comm_3 (a b c : ℝ) : a + b + c = c + b + a := sorry
+
+definition rep (x : ℝ) : reg_seq := some (quot.exists_rep x)
+
+definition const (a : ℚ) : ℝ := quot.mk (s.r_const a) 
+
+theorem add_consts (a b : ℚ) : const a + const b = const (a + b) := 
+  quot.sound (s.r_add_consts a b)
+
+theorem sub_consts (a b : ℚ) : const a - const b = const (a - b) := !add_consts
+
+theorem add_half_const (n : ℕ+) : const (2 * n)⁻¹ + const (2 * n)⁻¹ = const (n⁻¹) := 
+  by rewrite [add_consts, padd_halves]
+
+theorem const_le_const_of_le (a b : ℚ) : a ≤ b → const a ≤ const b := 
+  s.r_const_le_const_of_le
+
+theorem le_of_const_le_const (a b : ℚ) : const a ≤ const b → a ≤ b := 
+  s.r_le_of_const_le_const
+
+definition re_abs (x : ℝ) : ℝ := 
+  quot.lift_on x (λ a, quot.mk (s.r_abs a)) (take a b Hab, quot.sound (s.r_abs_well_defined Hab))
+
+theorem r_abs_nonneg {x : ℝ} : 0 ≤ x → re_abs x = x :=
+  quot.induction_on x (λ a Ha, quot.sound  (s.r_equiv_abs_of_ge_zero Ha))
+
+theorem r_abs_nonpos {x : ℝ} : x ≤ 0 → re_abs x = -x :=
+  quot.induction_on x (λ a Ha, quot.sound (s.r_equiv_neg_abs_of_le_zero Ha))
+
+theorem abs_const' (a : ℚ) : const (rat.abs a) = re_abs (const a) := quot.sound (s.r_abs_const a)
+
+theorem re_abs_is_abs : re_abs = algebra.abs := funext
+  (begin
+    intro x,
+    rewrite ↑abs,
+    apply eq.symm,
+    let Hor := decidable.em (0 ≤ x),
+    apply or.elim Hor,
+    intro Hor1,
+    rewrite [(if_pos Hor1), r_abs_nonneg Hor1],
+    intro Hor2,
+    let Hor2' := algebra.le_of_lt (algebra.lt_of_not_ge Hor2),
+    rewrite [(if_neg Hor2), r_abs_nonpos Hor2']
+  end)
+
+theorem abs_const (a : ℚ) : const (rat.abs a) = abs (const a) :=
+  by rewrite -re_abs_is_abs -- ????
+
+theorem rat_approx' (x : ℝ) : ∀ n : ℕ+, ∃ q : ℚ, re_abs (x - const q) ≤ const n⁻¹ :=
+  quot.induction_on x (λ s n, s.r_rat_approx s n)
+
+theorem rat_approx (x : ℝ) : ∀ n : ℕ+, ∃ q : ℚ, abs (x - const q) ≤ const n⁻¹ :=
+  by rewrite -re_abs_is_abs; apply rat_approx'
+
+definition approx (x : ℝ) (n : ℕ+) := some (rat_approx x n)
+
+theorem approx_spec (x : ℝ) (n : ℕ+) : abs (x - (const (approx x n))) ≤ const n⁻¹ := 
+  some_spec (rat_approx x n)
+
+theorem approx_spec' (x : ℝ) (n : ℕ+) : abs ((const (approx x n)) - x) ≤ const n⁻¹ :=
+  by rewrite algebra.abs_sub; apply approx_spec
+
+notation `r_seq` := ℕ+ → ℝ
+
+definition converges_to (X : r_seq) (a : ℝ) (N : ℕ+ → ℕ+) :=
+  ∀ k : ℕ+, ∀ n : ℕ+, n ≥ N k → abs (X n - a) ≤ const k⁻¹
+
+definition cauchy (X : r_seq) (M : ℕ+ → ℕ+) :=
+  ∀ k : ℕ+, ∀ m n : ℕ+, m ≥ M k → n ≥ M k → abs (X m - X n) ≤ const k⁻¹
+
+theorem cauchy_of_converges_to {X : r_seq} {a : ℝ} {N : ℕ+ → ℕ+} (Hc : converges_to X a N) :
+        cauchy X (λ k, N (2 * k)) :=
+  begin
+    intro k m n Hm Hn, 
+    rewrite (rewrite_helper9 a),
+    apply algebra.le.trans,
+    apply algebra.abs_add_le_abs_add_abs,
+    apply algebra.le.trans,
+    apply algebra.add_le_add,
+    apply Hc,
+    apply Hm,
+    rewrite algebra.abs_neg,
+    apply Hc,
+    apply Hn,
+    rewrite add_half_const,
+    apply !algebra.le.refl
+  end
+
+definition Nb (M : ℕ+ → ℕ+) := λ k, max (3 * k) (M (2 * k))
+
+theorem Nb_spec_right (M : ℕ+ → ℕ+) (k : ℕ+) : M (2 * k) ≤ Nb M k := !max_right
+
+theorem Nb_spec_left (M : ℕ+ → ℕ+) (k : ℕ+) : 3 * k ≤ Nb M k := !max_left
+
+definition lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : seq :=
+  λ k, approx (X (Nb M k)) (2 * k)
+
+theorem lim_seq_reg_helper {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) {m n : ℕ+} 
+        (Hmn : M (2 * n) ≤M (2 * m)) :
+           abs (const (lim_seq Hc m) - X (Nb M m)) + abs (X (Nb M m) - X (Nb M n)) + abs
+            (X (Nb M n) - const (lim_seq Hc n)) ≤ const (m⁻¹ + n⁻¹) :=
+  begin
+    apply algebra.le.trans,
+    apply r_add_le_add_three,
+    apply approx_spec',
+    rotate 1,
+    apply approx_spec,
+    rotate 1,
+    apply Hc,
+    rotate 1,
+    apply Nb_spec_right,
+    rotate 1,
+    apply ple.trans,
+    apply Hmn,
+    apply Nb_spec_right,
+    rewrite [*add_consts, rat.add.assoc, padd_halves],
+    apply const_le_const_of_le,
+    apply rat.add_le_add_right,
+    apply inv_ge_of_le,
+    apply pnat.mul_le_mul_left
+  end
+
+theorem lim_seq_reg {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : regular (lim_seq Hc) := 
+  begin
+    rewrite ↑regular,
+    intro m n,
+    apply le_of_const_le_const,
+    rewrite [abs_const, -sub_consts, (rewrite_helper10 (X (Nb M m)) (X (Nb M n)))],
+    apply algebra.le.trans,
+    apply r_abs_add_three,
+    let Hor := decidable.em (M (2 * m) ≥ M (2 * n)),
+    apply or.elim Hor,
+    intro Hor1,
+    apply lim_seq_reg_helper Hc Hor1,
+    intro Hor2,
+    let Hor2' := pnat.le_of_lt (pnat.lt_of_not_le Hor2),
+    rewrite [algebra.abs_sub (X (Nb M n)), algebra.abs_sub (X (Nb M m)), algebra.abs_sub, -- ???
+             rat.add.comm, re_add_comm_3],
+    apply lim_seq_reg_helper Hc Hor2'
+  end
+
+theorem lim_seq_spec {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) (k : ℕ+) : 
+        s.s_le (s.s_abs (sadd (lim_seq Hc) (sneg (s.const (lim_seq Hc k))) )) (s.const k⁻¹) :=
+  begin
+    apply s.const_bound,
+    apply lim_seq_reg
+  end
+
+definition r_lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : reg_seq :=
+  reg_seq.mk (lim_seq Hc) (lim_seq_reg Hc)
+
+theorem r_lim_seq_spec {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) (k : ℕ+) :
+        s.r_le (s.r_abs (((r_lim_seq Hc) + -s.r_const ((reg_seq.sq (r_lim_seq Hc)) k)))) (s.r_const (k)⁻¹) := 
+  lim_seq_spec Hc k
+
+definition lim {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : ℝ :=
+  quot.mk (r_lim_seq Hc)
+
+theorem re_lim_spec {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) : 
+        re_abs ((lim Hc) - (const ((lim_seq Hc) k))) ≤ const k⁻¹ :=
+  r_lim_seq_spec Hc k 
+
+theorem lim_spec' {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) : 
+        abs ((lim Hc) - (const ((lim_seq Hc) k))) ≤ const k⁻¹ :=
+  by rewrite -re_abs_is_abs; apply re_lim_spec
+
+theorem lim_spec {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) : 
+        abs ((const ((lim_seq Hc) k)) - (lim Hc)) ≤ const (k)⁻¹ :=
+  by rewrite algebra.abs_sub; apply lim_spec'
+
+theorem converges_of_cauchy {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : 
+        converges_to X (lim Hc) (Nb M) := 
+  begin
+    intro k n Hn,
+    rewrite (rewrite_helper10 (X (Nb M n)) (const (lim_seq Hc n))),
+    apply algebra.le.trans,
+    apply r_abs_add_three,
+    apply algebra.le.trans,
+    apply r_add_le_add_three,
+    apply Hc,
+    apply ple.trans,
+    rotate 1,
+    apply Hn,
+    rotate_right 1,
+    apply Nb_spec_right,
+    have HMk : M (2 * k) ≤ Nb M n, begin
+      apply ple.trans,
+      apply Nb_spec_right,
+      apply ple.trans,
+      apply Hn,
+      apply ple.trans,
+      apply pnat.mul_le_mul_left 3,
+      apply Nb_spec_left
+    end,
+    apply HMk,
+    rewrite ↑lim_seq,
+    apply approx_spec,
+    apply lim_spec,
+    rewrite 2 add_consts,
+    apply const_le_const_of_le,
+    apply rat.le.trans,
+    apply add_le_add_three,
+    apply rat.le.refl,
+    apply inv_ge_of_le,
+    apply pnat_mul_le_mul_left',
+    apply ple.trans,
+    rotate 1,
+    apply Hn,
+    rotate_right 1,
+    apply Nb_spec_left,
+    apply inv_ge_of_le,
+    apply ple.trans,
+    rotate 1,
+    apply Hn,
+    rotate_right 1,
+    apply Nb_spec_left,
+    rewrite [-*pnat_mul_assoc, p_add_fractions],
+    apply rat.le.refl
+  end
+
+end real

library/data/real/division.lean

@@ -568,6 +568,33 @@ theorem lt_or_equiv_of_le {s t : seq} (Hs : regular s) (Ht : regular t) (Hle : s
   if H : s ≡ t then or.inr H else
     or.inl (lt_of_le_and_sep Hs Ht (and.intro Hle (sep_of_nequiv Hs Ht H)))
 
+theorem s_le_of_equiv_le_left {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) 
+        (Heq : s ≡ t) (Hle : s_le s u) : s_le t u :=
+  begin
+    rewrite ↑s_le at *,
+    apply nonneg_of_nonneg_equiv,
+    rotate 2,
+    apply add_well_defined,
+    rotate 4,
+    apply equiv.refl,
+    apply neg_well_defined,
+    apply Heq,
+    repeat (assumption | apply reg_add_reg | apply reg_neg_reg)
+  end
+
+theorem s_le_of_equiv_le_right {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) 
+        (Heq : t ≡ u) (Hle : s_le s t) : s_le s u :=
+  begin
+    rewrite ↑s_le at *,
+    apply nonneg_of_nonneg_equiv,
+    rotate 2,
+    apply add_well_defined,
+    rotate 4,
+    apply Heq,
+    apply equiv.refl,
+    repeat (assumption | apply reg_add_reg | apply reg_neg_reg)
+  end
+
 -----------------------------
 
 definition r_inv (s : reg_seq) : reg_seq := reg_seq.mk (s_inv (reg_seq.is_reg s))  
@@ -593,6 +620,11 @@ theorem r_sep_of_nequiv (s t : reg_seq) (Hneq : ¬ requiv s t) : r_sep s t :=
 theorem r_lt_or_equiv_of_le (s t : reg_seq) (Hle : r_le s t) : r_lt s t ∨ requiv s t :=
   lt_or_equiv_of_le (reg_seq.is_reg s) (reg_seq.is_reg t) Hle
 
+theorem r_le_of_equiv_le_left {s t u : reg_seq} (Heq : requiv s t) (Hle : r_le s u) : r_le t u :=
+  s_le_of_equiv_le_left (reg_seq.is_reg s) (reg_seq.is_reg t) (reg_seq.is_reg u) Heq Hle
+
+theorem r_le_of_equiv_le_right {s t u : reg_seq} (Heq : requiv t u) (Hle : r_le s t) : r_le s u :=
+  s_le_of_equiv_le_right (reg_seq.is_reg s) (reg_seq.is_reg t) (reg_seq.is_reg u) Heq Hle
 
 end s
 
@@ -642,7 +674,8 @@ theorem dec_lt : decidable_rel lt :=
     apply prop_decidable
   end
 
-definition linear_ordered_field : algebra.discrete_linear_ordered_field ℝ :=
+open [classes] algebra
+definition linear_ordered_field [instance] : algebra.discrete_linear_ordered_field ℝ :=
   ⦃ algebra.discrete_linear_ordered_field, comm_ring, ordered_ring, 
     le_total := le_total,
     mul_inv_cancel := mul_inv,

library/data/real/order.lean

@@ -53,8 +53,7 @@ theorem bdd_away_of_pos {s : seq} (Hs : regular s) (H : pos s) :
     let Em := sep_by_inv Hn,
     apply exists.elim Em,
     intro N HN,
-    fapply exists.intro,
-    exact N,
+    existsi N,
     intro m Hm,
     have Habs : abs (s m - s n) ≥ s n - s m, by rewrite abs_sub; apply le_abs_self,
     have Habs' : s m + abs (s m - s n) ≥ s n, from (iff.mp' (le_add_iff_sub_left_le _ _ _)) Habs,
@@ -80,8 +79,7 @@ theorem pos_of_bdd_away {s : seq} (H : ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → (
     rewrite ↑pos,
     apply exists.elim H,
     intro N HN,
-    fapply exists.intro,
-    exact (N + pone),
+    existsi (N + pone),
     apply lt_of_lt_of_le,
     apply inv_add_lt_left,
     apply HN,
@@ -93,8 +91,7 @@ theorem bdd_within_of_nonneg {s : seq} (Hs : regular s) (H : nonneg s) :
         ∀ n : ℕ+, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → s m ≥ -n⁻¹ := 
   begin
     intros,
-    fapply exists.intro,
-    exact n,
+    existsi n,
     intro m Hm, 
     rewrite ↑nonneg at H,
     apply le.trans,
@@ -149,8 +146,7 @@ theorem pos_of_pos_equiv {s t : seq} (Hs : regular s) (Heq : s ≡ t) (Hp : pos
     rewrite [↑pos at *],
     apply exists.elim (bdd_away_of_pos Hs Hp),
     intro N HN,
-    fapply exists.intro,
-    exact 2 * 2 * N,
+    existsi 2 * 2 * N,
     apply lt_of_lt_of_le,
     rotate 1,
     apply ge_sub_of_abs_sub_le_right,
@@ -174,8 +170,7 @@ theorem nonneg_of_nonneg_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (He
     let Bd := (bdd_within_of_nonneg Hs Hp) (2 * 2 * n),
     apply exists.elim Bd,
     intro Ns HNs,
-    fapply exists.intro,
-    exact max Ns (2 * 2 * n),
+    existsi max Ns (2 * 2 * n),
     intro m Hm,
     apply le.trans,
     rotate 1,
@@ -223,8 +218,7 @@ theorem zero_nonneg : nonneg zero :=
 theorem s_zero_lt_one : s_lt zero one :=
   begin
     rewrite [↑s_lt, ↑zero, ↑sadd, ↑sneg, ↑one, neg_zero, add_zero, ↑pos],
-    fapply exists.intro,
-    exact 2,
+    existsi 2,
     apply inv_lt_one_of_gt,
     apply one_lt_two
   end
@@ -248,8 +242,7 @@ theorem s_nonneg_of_pos {s : seq} (Hs : regular s) (H : pos s) : nonneg s :=
     let Bt := bdd_away_of_pos Hs H,
     apply exists.elim Bt,
     intro N HN,
-    fapply exists.intro,
-    exact N,
+    existsi N,
     intro m Hm,
     apply le.trans,
     rotate 1,
@@ -533,8 +526,7 @@ theorem s_mul_pos_of_pos {s t : seq} (Hs : regular s) (Ht : regular t) (Hps : po
     intros Ns HNs,
     apply exists.elim (bdd_away_of_pos Ht Hpt),
     intros Nt HNt,
-    fapply exists.intro,
-    exact 2 * max Ns Nt * max Ns Nt,
+    existsi 2 * max Ns Nt * max Ns Nt,
     rewrite ↑smul,
     apply lt_of_lt_of_le,
     rotate 1,
@@ -835,8 +827,7 @@ theorem s_lt_of_lt_of_le {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
     apply exists.elim (bdd_within_of_nonneg Runt Htu (2 * Nt)),
     intro Nu HNu,
     apply pos_of_bdd_away,
-    fapply exists.intro,
-    exact max (2 * Nt) Nu,
+    existsi max (2 * Nt) Nu,
     intro n Hn,
     rewrite Hcan,
     apply rat.le.trans,
@@ -876,8 +867,7 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
     apply exists.elim (bdd_within_of_nonneg Rtns Hst (2 * Nu)),
     intro Nt HNt,
     apply pos_of_bdd_away,
-    fapply exists.intro,
-    exact max (2 * Nu) Nt,
+    existsi max (2 * Nu) Nt,
     intro n Hn,
     rewrite Hcan,
     apply rat.le.trans,