From 7a4947cfe125086541dc245cb7736be53ce49229 Mon Sep 17 00:00:00 2001
From: Rob Lewis <rob.y.lewis@gmail.com>
Date: Mon, 27 Jul 2015 18:33:34 -0400
Subject: [PATCH] feat(library/algebra/real): significant progress toward
 supremum property

---
 library/data/real/complete.lean | 60 +++++++++++++++++++++++++++++++--
 library/data/real/order.lean    |  1 -
 2 files changed, 57 insertions(+), 4 deletions(-)

diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean
index 2b3895ed46..d4a1dfd09e 100644
--- a/library/data/real/complete.lean
+++ b/library/data/real/complete.lean
@@ -509,7 +509,7 @@ definition under_seq' := λ n, under_seq (n + some width_narrows)
 
 theorem width' (n : ℕ) : over_seq' n - under_seq' n ≤ 1 / rat.pow 2 n := sorry
 
-theorem twos (y r : ℚ) (H : 0 < r) : ∃ n : ℕ, y / (rat.pow 2 n) < r := sorry
+--theorem twos (y r : ℚ) (H : 0 < r) : ∃ n : ℕ, y / (rat.pow 2 n) < r := sorry
 
 theorem PA (n : ℕ) : ¬ ub (under_seq n) :=
   nat.induction_on n
@@ -575,9 +575,63 @@ theorem dist_bdd_within_interval {a b lb ub : ℚ} (H : lb < ub) (Hal : lb ≤ a
 
 --theorem over_dist (n : ℕ) : abs (over - over_seq n) ≤ (over - under) / rat.pow 2 n := sorry
 
-theorem under_seq_mono : ∀ i j : ℕ, i ≤ j → under_seq i ≤ under_seq j := sorry
+theorem rat.div_le_div_of_le_of_pos {a b c : ℚ} (H : a ≤ b) (Hc : c > 0) : a / c ≤ b / c := sorry
 
-theorem over_seq_mono : ∀ i j : ℕ, i ≤ j → over_seq j ≤ over_seq i := sorry
+theorem under_seq_mono_helper (i k : ℕ) : under_seq i ≤ under_seq (i + k) :=
+  (nat.induction_on k
+    (by rewrite nat.add_zero; apply rat.le.refl)
+    (begin
+      intros a Ha,
+      rewrite [add_succ, under_succ],
+      cases (decidable.em (ub (avg_seq (i + a)))) with [Havg, Havg],
+      rewrite (if_pos Havg),
+      apply Ha,
+      rewrite [if_neg Havg, ↑avg_seq, ↑avg],
+      apply rat.le.trans,
+      apply Ha,
+      rewrite -rat.add_halves at {1},
+      apply rat.add_le_add_right,
+      apply rat.div_le_div_of_le_of_pos,
+      apply rat.le_of_lt,
+      apply under_seq_lt_over_seq,
+      apply dec_trivial
+    end))
+
+theorem under_seq_mono (i j : ℕ) (H : i ≤ j) : under_seq i ≤ under_seq j :=
+  begin
+    cases le.elim H with [k, Hk'],
+    rewrite -Hk',
+    apply under_seq_mono_helper
+  end
+
+theorem over_seq_mono_helper (i k : ℕ) : over_seq (i + k) ≤ over_seq i :=
+  nat.induction_on k
+    (by rewrite nat.add_zero; apply rat.le.refl)
+    (begin
+      intros a Ha,
+      rewrite [add_succ, over_succ],
+      cases (decidable.em (ub (avg_seq (i + a)))) with [Havg, Havg],
+      rewrite [if_pos Havg, ↑avg_seq, ↑avg],
+      apply rat.le.trans,
+      rotate 1,
+      apply Ha,
+      rotate 1,
+      rewrite -{over_seq (i + a)}rat.add_halves at {2},
+      apply rat.add_le_add_left,
+      apply rat.div_le_div_of_le_of_pos,
+      apply rat.le_of_lt,
+      apply under_seq_lt_over_seq,
+      apply dec_trivial,
+      rewrite [if_neg Havg],
+      apply Ha
+    end)
+
+theorem over_seq_mono (i j : ℕ) (H : i ≤ j) : over_seq j ≤ over_seq i :=
+  begin
+    cases le.elim H with [k, Hk'],
+    rewrite -Hk',
+    apply over_seq_mono_helper
+  end
 
 theorem rat_power_two_le (k : ℕ+) : rat_of_pnat k ≤ rat.pow 2 k~ := sorry
 
diff --git a/library/data/real/order.lean b/library/data/real/order.lean
index cf1ca49969..cc43862fa8 100644
--- a/library/data/real/order.lean
+++ b/library/data/real/order.lean
@@ -1212,7 +1212,6 @@ theorem lt_of_rat_lt_of_rat (a b : ℚ) : of_rat a < of_rat b → a < b :=
 theorem of_rat_sub (a b : ℚ) : of_rat a - of_rat b = of_rat (a - b) := rfl
 
 open s
-set_option pp.coercions true
 theorem le_of_le_reprs (x : ℝ) (t : seq) (Ht : regular t) : (∀ n : ℕ+, x ≤ t n) →
         x ≤ quot.mk (reg_seq.mk t Ht) :=
   quot.induction_on x (take s Hs,