refactor(library/data/real): move and rename theorems

library/algebra/ordered_field.lean

@@ -342,6 +342,15 @@ section linear_ordered_field
            exact H3)
       (div_pos_of_pos_of_pos (iff.mpr !sub_pos_iff_lt H) two_pos))
 
+  theorem ge_of_forall_ge_sub {a b : A} (H : ∀ ε : A, ε > 0 → a ≥ b - ε) : a ≥ b :=
+   begin
+    apply le_of_not_gt,
+    intro Hb,
+    cases exists_add_lt_and_pos_of_lt Hb with [c, Hc],
+    let Hc' := H c (and.right Hc),
+    apply (not_le_of_gt (and.left Hc)) (iff.mpr !le_add_iff_sub_right_le Hc')
+   end
+
 end linear_ordered_field
 
 structure discrete_linear_ordered_field [class] (A : Type) extends linear_ordered_field A,

library/data/int/order.lean

@@ -388,5 +388,80 @@ dvd.elim H'
   (take b,
     suppose 1 = a * b,
     eq_one_of_mul_eq_one_right H this⁻¹)
+--
+
+theorem ex_smallest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] (Hbdd : ∃ b : ℤ, ∀ z : ℤ, z ≤ b → ¬ P z)
+        (Hinh : ∃ z : ℤ, P z) : ∃ lb : ℤ, P lb ∧ (∀ z : ℤ, z < lb → ¬ P z) :=
+  begin
+    cases Hbdd with [b, Hb],
+    cases Hinh with [elt, Helt],
+    existsi b + of_nat (least (λ n, P (b + of_nat n)) (nat.succ (nat_abs (elt - b)))),
+    have Heltb : elt > b, begin
+      apply int.lt_of_not_ge,
+      intro Hge,
+      apply (Hb _ Hge) Helt
+    end,
+    have H' : P (b + of_nat (nat_abs (elt - b))), begin
+      rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !int.sub_pos_iff_lt Heltb)),
+              int.add.comm, int.sub_add_cancel],
+      apply Helt
+    end,
+    apply and.intro,
+    apply least_of_lt _ !lt_succ_self H',
+    intros z Hz,
+    cases em (z ≤ b) with [Hzb, Hzb],
+    apply Hb _ Hzb,
+    let Hzb' := int.lt_of_not_ge Hzb,
+    let Hpos := iff.mpr !int.sub_pos_iff_lt Hzb',
+    have Hzbk : z = b + of_nat (nat_abs (z - b)),
+      by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.add.comm, int.sub_add_cancel],
+    have Hk : nat_abs (z - b) < least (λ n, P (b + of_nat n)) (nat.succ (nat_abs (elt - b))), begin
+     let Hz' := iff.mp !int.lt_add_iff_sub_lt_left Hz,
+     rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'],
+     apply iff.mp !int.of_nat_lt_of_nat Hz'
+    end,
+    let Hk' := nat.not_le_of_gt Hk,
+    rewrite Hzbk,
+    apply λ p, mt (ge_least_of_lt _ p) Hk',
+    apply nat.lt.trans Hk,
+    apply least_lt _ !lt_succ_self H'
+  end
+
+theorem ex_largest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] (Hbdd : ∃ b : ℤ, ∀ z : ℤ, z ≥ b → ¬ P z)
+        (Hinh : ∃ z : ℤ, P z) : ∃ ub : ℤ, P ub ∧ (∀ z : ℤ, z > ub → ¬ P z) :=
+  begin
+    cases Hbdd with [b, Hb],
+    cases Hinh with [elt, Helt],
+    existsi b - of_nat (least (λ n, P (b - of_nat n)) (nat.succ (nat_abs (b - elt)))),
+    have Heltb : elt < b, begin
+      apply int.lt_of_not_ge,
+      intro Hge,
+      apply (Hb _ Hge) Helt
+    end,
+    have H' : P (b - of_nat (nat_abs (b - elt))), begin
+      rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !int.sub_pos_iff_lt Heltb)),
+              int.sub_sub_self],
+      apply Helt
+    end,
+    apply and.intro,
+    apply least_of_lt _ !lt_succ_self H',
+    intros z Hz,
+    cases em (z ≥ b) with [Hzb, Hzb],
+    apply Hb _ Hzb,
+    let Hzb' := int.lt_of_not_ge Hzb,
+    let Hpos := iff.mpr !int.sub_pos_iff_lt Hzb',
+    have Hzbk : z = b - of_nat (nat_abs (b - z)),
+      by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.sub_sub_self],
+    have Hk : nat_abs (b - z) < least (λ n, P (b - of_nat n)) (nat.succ (nat_abs (b - elt))), begin
+      let Hz' := iff.mp !int.lt_add_iff_sub_lt_left (iff.mpr !int.lt_add_iff_sub_lt_right Hz),
+      rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'],
+      apply iff.mp !int.of_nat_lt_of_nat Hz'
+    end,
+    let Hk' := nat.not_le_of_gt Hk,
+    rewrite Hzbk,
+    apply λ p, mt (ge_least_of_lt _ p) Hk',
+    apply nat.lt.trans Hk,
+    apply least_lt _ !lt_succ_self H'
+  end
 
 end int

library/data/pnat.lean

@@ -312,4 +312,18 @@ theorem nonneg_of_ge_neg_invs (a : ℚ) (H : ∀ n : ℕ+, -n⁻¹ ≤ a) : 0
           : div_lt_div_of_pos_of_lt_of_pos dec_trivial dec_trivial H2
                              ... = -a : !div_one)))
 
+theorem pnat_bound {ε : ℚ} (Hε : ε > 0) : ∃ p : ℕ+, p⁻¹ ≤ ε :=
+  begin
+    existsi (pceil (1 / ε)),
+    rewrite -(rat.one_div_one_div ε) at {2},
+    apply pceil_helper,
+    apply le.refl,
+    apply one_div_pos_of_pos Hε
+  end
+
+theorem p_add_fractions (n : ℕ+) : (2 * n)⁻¹ + (2 * 3 * n)⁻¹ + (3 * n)⁻¹ = n⁻¹ :=
+  assert T : 2⁻¹ + 2⁻¹ * 3⁻¹ + 3⁻¹ = 1, from dec_trivial,
+  by rewrite[*inv_mul_eq_mul_inv,-*rat.right_distrib,T,rat.one_mul]
+
+
 end pnat

library/data/real/basic.lean

@@ -5,8 +5,20 @@ Author: Robert Y. Lewis
 The real numbers, constructed as equivalence classes of Cauchy sequences of rationals.
 This construction follows Bishop and Bridges (1985).
 
-To do:
- o Rename things and possibly make theorems private
+The construction of the reals is arranged in four files.
+
+- basic.lean proves properties about regular sequences of rationals in the namespace rat_seq,
+  defines ℝ to be the quotient type of regular sequences mod equivalence, and shows ℝ is a ring
+  in namespace real. No classical axioms are used.
+
+- order.lean defines an order on regular sequences and lifts the order to ℝ. In the namespace real,
+  ℝ is shown to be an ordered ring. No classical axioms are used.
+
+- division.lean defines the inverse of a regular sequence and lifts this to ℝ. If a sequence is
+  equivalent to the 0 sequence, its inverse is the zero sequence. In the namespace real, ℝ is shown
+  to be an ordered field. This construction is classical.
+
+- complete.lean
 -/
 import data.nat data.rat.order data.pnat
 open nat eq eq.ops pnat
@@ -16,11 +28,11 @@ local notation 1 := rat.of_num 1
 
 -- small helper lemmas
 
-theorem s_mul_assoc_lemma_3 (a b n : ℕ+) (p : ℚ) :
+private theorem s_mul_assoc_lemma_3 (a b n : ℕ+) (p : ℚ) :
         p * ((a * n)⁻¹ + (b * n)⁻¹) = p * (a⁻¹ + b⁻¹) * n⁻¹ :=
   by rewrite [rat.mul.assoc, rat.right_distrib, *inv_mul_eq_mul_inv]
 
-theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq : q > 0) (H : n ≥ pceil (q / ε)) :
+private theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq : q > 0) (H : n ≥ pceil (q / ε)) :
         q * n⁻¹ ≤ ε :=
   begin
     let H2 := pceil_helper H (div_pos_of_pos_of_pos Hq Hε),
@@ -30,7 +42,7 @@ theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq : q > 0)
     repeat assumption
   end
 
-theorem find_thirds (a b : ℚ) (H : b > 0) : ∃ n : ℕ+, a + n⁻¹ + n⁻¹ + n⁻¹ < a + b :=
+private theorem find_thirds (a b : ℚ) (H : b > 0) : ∃ n : ℕ+, a + n⁻¹ + n⁻¹ + n⁻¹ < a + b :=
   let n := pceil (of_nat 4 / b) in
   have of_nat 3 * n⁻¹ < b, from calc
    of_nat 3 * n⁻¹ < of_nat 4 * n⁻¹
@@ -44,7 +56,7 @@ theorem find_thirds (a b : ℚ) (H : b > 0) : ∃ n : ℕ+, a + n⁻¹ + n⁻¹
                     ... = a + of_nat 3 * n⁻¹    : {show 1+1+1=of_nat 3, from dec_trivial}
                     ... < a + b                 : rat.add_lt_add_left this a)
 
-theorem squeeze {a b : ℚ} (H : ∀ j : ℕ+, a ≤ b + j⁻¹ + j⁻¹ + j⁻¹) : a ≤ b :=
+private theorem squeeze {a b : ℚ} (H : ∀ j : ℕ+, a ≤ b + j⁻¹ + j⁻¹ + j⁻¹) : a ≤ b :=
   begin
     apply rat.le_of_not_gt,
     intro Hb,
@@ -54,29 +66,20 @@ theorem squeeze {a b : ℚ} (H : ∀ j : ℕ+, a ≤ b + j⁻¹ + j⁻¹ + j⁻
     apply (not_le_of_gt Ha) !H
   end
 
-theorem squeeze_2 {a b : ℚ} (H : ∀ ε : ℚ, ε > 0 → a ≥ b - ε) : a ≥ b :=
-  begin
-    apply rat.le_of_not_gt,
-    intro Hb,
-    cases exists_add_lt_and_pos_of_lt Hb with [c, Hc],
-    let Hc' := H c (and.right Hc),
-    apply (rat.not_le_of_gt (and.left Hc)) (iff.mpr !le_add_iff_sub_right_le Hc')
-  end
-
-theorem rewrite_helper (a b c d : ℚ) : a * b  - c * d = a * (b - d) + (a - c) * d :=
+private theorem rewrite_helper (a b c d : ℚ) : a * b  - c * d = a * (b - d) + (a - c) * d :=
   by rewrite[rat.mul_sub_left_distrib, rat.mul_sub_right_distrib, add_sub, rat.sub_add_cancel]
 
-theorem rewrite_helper3 (a b c d e f g: ℚ) : a * (b + c) - (d * e + f * g) =
+private theorem rewrite_helper3 (a b c d e f g: ℚ) : a * (b + c) - (d * e + f * g) =
         (a * b - d * e) + (a * c - f * g) :=
   by rewrite[rat.mul.left_distrib, add_sub_comm]
 
-theorem rewrite_helper4 (a b c d : ℚ) : a * b - c * d = (a * b - a * d) + (a * d - c * d) :=
+private theorem rewrite_helper4 (a b c d : ℚ) : a * b - c * d = (a * b - a * d) + (a * d - c * d) :=
   by rewrite[add_sub, rat.sub_add_cancel]
 
-theorem rewrite_helper5 (a b x y : ℚ) : a - b = (a - x) + (x - y) + (y - b) :=
+private theorem rewrite_helper5 (a b x y : ℚ) : a - b = (a - x) + (x - y) + (y - b) :=
   by rewrite[*add_sub, *rat.sub_add_cancel]
 
-theorem rewrite_helper7 (a b c d x : ℚ) :
+private theorem rewrite_helper7 (a b c d x : ℚ) :
         a * b * c - d = (b * c) * (a - x) + (x * b * c - d) :=
   by rewrite[rat.mul_sub_left_distrib, add_sub]; exact (calc
      a * b * c - d = a * b * c - x * b * c + x * b * c - d : rat.sub_add_cancel
@@ -85,7 +88,7 @@ theorem rewrite_helper7 (a b c d x : ℚ) :
          λa b c, !rat.mul.comm ▸ !rat.mul.right_comm,
        this ▸ this ▸ rfl)
 
-theorem ineq_helper (a b : ℚ) (k m n : ℕ+) (H : a ≤ (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹)
+private theorem ineq_helper (a b : ℚ) (k m n : ℕ+) (H : a ≤ (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹)
                     (H2 : b ≤ (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹) :
         (rat_of_pnat k) * a + b * (rat_of_pnat k) ≤ m⁻¹ + n⁻¹ :=
   have (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹ = (2 * k)⁻¹ * (m⁻¹ + n⁻¹),
@@ -101,19 +104,19 @@ theorem ineq_helper (a b : ℚ) (k m n : ℕ+) (H : a ≤ (k * 2 * m)⁻¹ + (k
              iff.mp (!rat.le_iff_mul_le_mul_left !rat_of_pnat_is_pos) this
      ... = m⁻¹ + n⁻¹ : by rewrite[-rat.mul.assoc, inv_cancel_left, rat.one_mul]
 
-theorem factor_lemma (a b c d e : ℚ) : abs (a + b + c - (d + (b + e))) = abs ((a - d) + (c - e)) :=
+private theorem factor_lemma (a b c d e : ℚ) : abs (a + b + c - (d + (b + e))) = abs ((a - d) + (c - e)) :=
   !congr_arg (calc
     a + b + c - (d + (b + e)) = a + b + c - (d + b + e)   : rat.add.assoc
                          ...  = a + b - (d + b) + (c - e) : add_sub_comm
                          ...  = a + b - b - d + (c - e)   : sub_add_eq_sub_sub_swap
                          ...  = a - d + (c - e)           : rat.add_sub_cancel)
 
-theorem factor_lemma_2 (a b c d : ℚ) : (a + b) + (c + d) = (a + c) + (d + b) :=
+private theorem factor_lemma_2 (a b c d : ℚ) : (a + b) + (c + d) = (a + c) + (d + b) :=
   !rat.add.comm ▸ (binary.comm4 rat.add.comm rat.add.assoc a b c d)
 
 --------------------------------------
 -- define cauchy sequences and equivalence. show equivalence actually is one
-namespace s
+namespace rat_seq
 
 notation `seq` := ℕ+ → ℚ
 
@@ -199,15 +202,6 @@ theorem eq_of_bdd_var {s t : seq} (Hs : regular s) (Ht : regular t)
     apply inv_pos
   end
 
-theorem pnat_bound {ε : ℚ} (Hε : ε > 0) : ∃ p : ℕ+, p⁻¹ ≤ ε :=
-  begin
-    existsi (pceil (1 / ε)),
-    rewrite -(rat.one_div_one_div ε) at {2},
-    apply pceil_helper,
-    apply le.refl,
-    apply one_div_pos_of_pos Hε
-  end
-
 theorem bdd_of_eq_var {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡ t) :
         ∀ ε : ℚ, ε > 0 → ∃ Nj : ℕ+, ∀ n : ℕ+, Nj ≤ n → abs (s n - t n) ≤ ε :=
   begin
@@ -240,9 +234,9 @@ theorem equiv.trans (s t u : seq) (Hs : regular s) (Ht : regular t) (Hu : regula
 -----------------------------------
 -- define operations on cauchy sequences. show operations preserve regularity
 
-definition K (s : seq) : ℕ+ := pnat.pos (ubound (abs (s pone)) + 1 + 1) dec_trivial
+private definition K (s : seq) : ℕ+ := pnat.pos (ubound (abs (s pone)) + 1 + 1) dec_trivial
 
-theorem canon_bound {s : seq} (Hs : regular s) (n : ℕ+) : abs (s n) ≤ rat_of_pnat (K s) :=
+private theorem canon_bound {s : seq} (Hs : regular s) (n : ℕ+) : abs (s n) ≤ rat_of_pnat (K s) :=
   calc
     abs (s n) = abs (s n - s pone + s pone) : by rewrite rat.sub_add_cancel
     ... ≤ abs (s n - s pone) + abs (s pone) : abs_add_le_abs_add_abs
@@ -278,7 +272,7 @@ theorem bdd_of_regular_strict {s : seq} (H : regular s) : ∃ b : ℚ, ∀ n :
 
 definition K₂ (s t : seq) := max (K s) (K t)
 
-theorem K₂_symm (s t : seq) : K₂ s t = K₂ t s :=
+private theorem K₂_symm (s t : seq) : K₂ s t = K₂ t s :=
   if H : K s < K t then
     (assert H1 : K₂ s t = K t, from max_eq_right H,
      assert H2 : K₂ t s = K t, from max_eq_left (not_lt_of_ge (le_of_lt H)),
@@ -394,15 +388,15 @@ theorem s_mul_comm (s t : seq) : smul s t ≡ smul t s :=
     apply add_invs_nonneg
   end
 
-definition DK (s t : seq) := (K₂ s t) * 2
-theorem DK_rewrite (s t : seq) : (K₂ s t) * 2 = DK s t := rfl
+private definition DK (s t : seq) := (K₂ s t) * 2
+private theorem DK_rewrite (s t : seq) : (K₂ s t) * 2 = DK s t := rfl
 
-definition TK (s t u : seq) := (DK (λ (n : ℕ+), s (mul (DK s t) n) * t (mul (DK s t) n)) u)
+private definition TK (s t u : seq) := (DK (λ (n : ℕ+), s (mul (DK s t) n) * t (mul (DK s t) n)) u)
 
-theorem TK_rewrite (s t u : seq) :
+private theorem TK_rewrite (s t u : seq) :
         (DK (λ (n : ℕ+), s (mul (DK s t) n) * t (mul (DK s t) n)) u) = TK s t u := rfl
 
-theorem s_mul_assoc_lemma (s t u : seq) (a b c d : ℕ+) :
+private theorem s_mul_assoc_lemma (s t u : seq) (a b c d : ℕ+) :
         abs (s a * t a * u b - s c * t d * u d) ≤ abs (t a) * abs (u b) * abs (s a - s c) +
                abs (s c) * abs (t a) * abs (u b - u d) + abs (s c) * abs (u d) * abs (t a - t d) :=
   begin
@@ -424,8 +418,8 @@ theorem s_mul_assoc_lemma (s t u : seq) (a b c d : ℕ+) :
     apply abs_nonneg
   end
 
-definition Kq (s : seq) := rat_of_pnat (K s) + 1
-theorem Kq_bound {s : seq} (H : regular s) : ∀ n, abs (s n) ≤ Kq s :=
+private definition Kq (s : seq) := rat_of_pnat (K s) + 1
+private theorem Kq_bound {s : seq} (H : regular s) : ∀ n, abs (s n) ≤ Kq s :=
   begin
     intros,
     apply rat.le_of_lt,
@@ -435,14 +429,14 @@ theorem Kq_bound {s : seq} (H : regular s) : ∀ n, abs (s n) ≤ Kq s :=
     apply rat.zero_lt_one
   end
 
-theorem Kq_bound_nonneg {s : seq} (H : regular s) : 0 ≤ Kq s :=
+private theorem Kq_bound_nonneg {s : seq} (H : regular s) : 0 ≤ Kq s :=
   rat.le.trans !abs_nonneg (Kq_bound H 2)
 
-theorem Kq_bound_pos {s : seq} (H : regular s) : 0 < Kq s :=
+private theorem Kq_bound_pos {s : seq} (H : regular s) : 0 < Kq s :=
   have H1 : 0 ≤ rat_of_pnat (K s), from rat.le.trans (!abs_nonneg) (canon_bound H 2),
   add_pos_of_nonneg_of_pos H1 rat.zero_lt_one
 
-theorem s_mul_assoc_lemma_5 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
+private theorem s_mul_assoc_lemma_5 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
     (a b c : ℕ+) : abs (t a) * abs (u b) * abs (s a - s c) ≤ (Kq t) * (Kq u) * (a⁻¹ + c⁻¹) :=
   begin
     repeat apply rat.mul_le_mul,
@@ -457,7 +451,7 @@ theorem s_mul_assoc_lemma_5 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu
     apply Kq_bound_nonneg Hu,
   end
 
-theorem s_mul_assoc_lemma_2 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
+private theorem s_mul_assoc_lemma_2 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
   (a b c d : ℕ+) :
      abs (t a) * abs (u b) * abs (s a - s c) + abs (s c) * abs (t a) * abs (u b - u d)
                + abs (s c) * abs (u d) * abs (t a - t d) ≤
@@ -589,7 +583,7 @@ theorem add_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu :
   end
 
 set_option tactic.goal_names false
-theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c : ℕ+) (j : ℕ+) :
+private theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c : ℕ+) (j : ℕ+) :
         ∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → abs (s (a * n) * t (b * n) - s (c * n) * t (c * n)) ≤ j⁻¹ :=
   begin
     existsi pceil (((rat_of_pnat (K s)) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) *
@@ -717,13 +711,13 @@ theorem mul_zero_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t) (Htz :
     apply rat.le.refl
   end
 
-theorem neg_bound_eq_bound (s : seq) : K (sneg s) = K s  :=
+private theorem neg_bound_eq_bound (s : seq) : K (sneg s) = K s  :=
   by rewrite [↑K, ↑sneg, abs_neg]
 
-theorem neg_bound2_eq_bound2 (s t : seq) : K₂ s (sneg t) = K₂ s t :=
+private theorem neg_bound2_eq_bound2 (s t : seq) : K₂ s (sneg t) = K₂ s t :=
   by rewrite [↑K₂, neg_bound_eq_bound]
 
-theorem sneg_def (s : seq) : (λ (n : ℕ+), -(s n)) = sneg s := rfl
+private theorem sneg_def (s : seq) : (λ (n : ℕ+), -(s n)) = sneg s := rfl
 
 theorem mul_neg_equiv_neg_mul {s t : seq} : smul s (sneg t) ≡ sneg (smul s t) :=
   begin
@@ -785,7 +779,7 @@ theorem diff_equiv_zero_of_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (
     repeat (assumption | apply reg_add_reg | apply reg_neg_reg)
   end
 
-theorem mul_well_defined_half1 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
+private theorem mul_well_defined_half1 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
         (Etu : t ≡ u) : smul s t ≡ smul s u :=
   begin
     apply equiv_of_diff_equiv_zero,
@@ -809,7 +803,7 @@ theorem mul_well_defined_half1 {s t u : seq} (Hs : regular s) (Ht : regular t) (
             apply zero_is_reg)
   end
 
-theorem mul_well_defined_half2 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
+private theorem mul_well_defined_half2 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
         (Est : s ≡ t) : smul s u ≡ smul t u :=
   begin
     apply equiv.trans,
@@ -1001,11 +995,11 @@ theorem r_mul_consts (a b : ℚ) : requiv (r_const a * r_const b) (r_const (a *
 
 theorem r_neg_const (a : ℚ) : requiv (-r_const a) (r_const (-a)) := neg_const a
 
-end s
+end rat_seq
 ----------------------------------------------
 -- take quotients to get ℝ and show it's a comm ring
 
-open s
+open rat_seq
 definition real := quot reg_seq.to_setoid
 namespace real
 notation `ℝ` := real
@@ -1030,7 +1024,7 @@ prefix [priority real.prio] `-` := neg
 
 open rat -- no coercions before
 
-definition of_rat [coercion] (a : ℚ) : ℝ := quot.mk (s.r_const a)
+definition of_rat [coercion] (a : ℚ) : ℝ := quot.mk (r_const a)
 definition of_num [coercion] [reducible] (n : num) : ℝ := of_rat (rat.of_num n)
 
 --definition zero : ℝ := 0
@@ -1099,12 +1093,12 @@ protected definition comm_ring [reducible] : algebra.comm_ring ℝ :=
   end
 
 theorem of_rat_add (a b : ℚ) : of_rat a + of_rat b = of_rat (a + b) :=
-   quot.sound (s.r_add_consts a b)
+   quot.sound (r_add_consts a b)
 
-theorem of_rat_neg (a : ℚ) : of_rat (-a) = -of_rat a := eq.symm (quot.sound (s.r_neg_const a))
+theorem of_rat_neg (a : ℚ) : of_rat (-a) = -of_rat a := eq.symm (quot.sound (r_neg_const a))
 
 theorem of_rat_mul (a b : ℚ) : of_rat a * of_rat b = of_rat (a * b) :=
-  quot.sound (s.r_mul_consts a b)
+  quot.sound (r_mul_consts a b)
 
 theorem add_half_of_rat (n : ℕ+) : of_rat (2 * n)⁻¹ + of_rat (2 * n)⁻¹ = of_rat (n⁻¹) :=
   by rewrite [of_rat_add, pnat.add_halves]

library/data/real/complete.lean

@@ -21,9 +21,9 @@ open eq.ops pnat classical
 local notation 2 := subtype.tag (nat.of_num 2) dec_trivial
 local notation 3 := subtype.tag (nat.of_num 3) dec_trivial
 
-namespace s
+namespace rat_seq
 
-theorem rat_approx_l1 {s : seq} (H : regular s) :
+theorem rat_approx {s : seq} (H : regular s) :
         ∀ n : ℕ+, ∃ q : ℚ, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → abs (s m - q) ≤ n⁻¹ :=
   begin
     intro n,
@@ -37,12 +37,12 @@ theorem rat_approx_l1 {s : seq} (H : regular s) :
     apply inv_ge_of_le Hm
   end
 
-theorem rat_approx {s : seq} (H : regular s) :
+theorem rat_approx_seq {s : seq} (H : regular s) :
         ∀ n : ℕ+, ∃ q : ℚ, s_le (s_abs (sadd s (sneg (const q)))) (const n⁻¹) :=
   begin
     intro m,
     rewrite ↑s_le,
-    cases rat_approx_l1 H m with [q, Hq],
+    cases rat_approx H m with [q, Hq],
     cases Hq with [N, HN],
     existsi q,
     apply nonneg_of_bdd_within,
@@ -66,26 +66,9 @@ theorem rat_approx {s : seq} (H : regular s) :
     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)
+  rat_approx_seq (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⁻¹) :=
@@ -176,35 +159,31 @@ theorem r_equiv_abs_of_ge_zero {s : reg_seq} (Hz : r_le r_zero s) : requiv (r_ab
 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
+end rat_seq
 
 namespace real
-open [classes] s
+open [classes] rat_seq
 
-theorem p_add_fractions (n : ℕ+) : (2 * n)⁻¹ + (2 * 3 * n)⁻¹ + (3 * n)⁻¹ = n⁻¹ :=
-  assert T : 2⁻¹ + 2⁻¹ * 3⁻¹ + 3⁻¹ = 1, from dec_trivial,
-  by rewrite[*inv_mul_eq_mul_inv,-*rat.right_distrib,T,rat.one_mul]
-
-theorem rewrite_helper9 (a b c : ℝ) : b - c = (b - a) - (c - a) :=
+private theorem rewrite_helper9 (a b c : ℝ) : b - c = (b - a) - (c - a) :=
   by rewrite[-sub_add_eq_sub_sub_swap,sub_add_cancel]
 
-theorem rewrite_helper10 (a b c d : ℝ) : c - d = (c - a) + (a - b) + (b - d) :=
+private theorem rewrite_helper10 (a b c d : ℝ) : c - d = (c - a) + (a - b) + (b - d) :=
   by rewrite[*add_sub,*sub_add_cancel]
 
-noncomputable definition rep (x : ℝ) : s.reg_seq := some (quot.exists_rep x)
+noncomputable definition rep (x : ℝ) : rat_seq.reg_seq := some (quot.exists_rep x)
 
 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))
+  quot.lift_on x (λ a, quot.mk (rat_seq.r_abs a)) (take a b Hab, quot.sound (rat_seq.r_abs_well_defined Hab))
 
 theorem r_abs_nonneg {x : ℝ} : zero ≤ x → re_abs x = x :=
-  quot.induction_on x (λ a Ha, quot.sound  (s.r_equiv_abs_of_ge_zero Ha))
+  quot.induction_on x (λ a Ha, quot.sound  (rat_seq.r_equiv_abs_of_ge_zero Ha))
 
 theorem r_abs_nonpos {x : ℝ} : x ≤ zero → re_abs x = -x :=
-  quot.induction_on x (λ a Ha, quot.sound (s.r_equiv_neg_abs_of_le_zero Ha))
+  quot.induction_on x (λ a Ha, quot.sound (rat_seq.r_equiv_neg_abs_of_le_zero Ha))
 
-theorem abs_const' (a : ℚ) : of_rat (rat.abs a) = re_abs (of_rat a) := quot.sound (s.r_abs_const a)
+private theorem abs_const' (a : ℚ) : of_rat (rat.abs a) = re_abs (of_rat a) := quot.sound (rat_seq.r_abs_const a)
 
-theorem re_abs_is_abs : re_abs = real.abs := funext
+private theorem re_abs_is_abs : re_abs = real.abs := funext
   (begin
     intro x,
     apply eq.symm,
@@ -217,8 +196,8 @@ theorem re_abs_is_abs : re_abs = real.abs := funext
 theorem abs_const (a : ℚ) : of_rat (rat.abs a) = abs (of_rat a) :=
   by rewrite -re_abs_is_abs
 
-theorem rat_approx' (x : ℝ) : ∀ n : ℕ+, ∃ q : ℚ, re_abs (x - of_rat q) ≤ of_rat n⁻¹ :=
-  quot.induction_on x (λ s n, s.r_rat_approx s n)
+private theorem rat_approx' (x : ℝ) : ∀ n : ℕ+, ∃ q : ℚ, re_abs (x - of_rat q) ≤ of_rat n⁻¹ :=
+  quot.induction_on x (λ s n, rat_seq.r_rat_approx s n)
 
 theorem rat_approx (x : ℝ) : ∀ n : ℕ+, ∃ q : ℚ, abs (x - of_rat q) ≤ of_rat n⁻¹ :=
   by rewrite -re_abs_is_abs; apply rat_approx'
@@ -259,11 +238,11 @@ theorem cauchy_of_converges_to {X : r_seq} {a : ℝ} {N : ℕ+ → ℕ+} (Hc : c
     apply rat.le.refl
   end
 
-definition Nb (M : ℕ+ → ℕ+) := λ k, pnat.max (3 * k) (M (2 * k))
+private definition Nb (M : ℕ+ → ℕ+) := λ k, pnat.max (3 * k) (M (2 * k))
 
-theorem Nb_spec_right (M : ℕ+ → ℕ+) (k : ℕ+) : M (2 * k) ≤ Nb M k := !max_right
+private 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
+private theorem Nb_spec_left (M : ℕ+ → ℕ+) (k : ℕ+) : 3 * k ≤ Nb M k := !max_left
 
 section lim_seq
 parameter {X : r_seq}
@@ -274,7 +253,7 @@ include Hc
 noncomputable definition lim_seq : ℕ+ → ℚ :=
   λ k, approx (X (Nb M k)) (2 * k)
 
-theorem lim_seq_reg_helper {m n : ℕ+} (Hmn : M (2 * n) ≤M (2 * m)) :
+private theorem lim_seq_reg_helper {m n : ℕ+} (Hmn : M (2 * n) ≤M (2 * m)) :
            abs (of_rat (lim_seq m) - X (Nb M m)) + abs (X (Nb M m) - X (Nb M n)) + abs
             (X (Nb M n) - of_rat (lim_seq n)) ≤ of_rat (m⁻¹ + n⁻¹) :=
   begin
@@ -298,9 +277,9 @@ theorem lim_seq_reg_helper {m n : ℕ+} (Hmn : M (2 * n) ≤M (2 * m)) :
     apply pnat.mul_le_mul_left
   end
 
-theorem lim_seq_reg : s.regular lim_seq :=
+theorem lim_seq_reg : rat_seq.regular lim_seq :=
   begin
-    rewrite ↑s.regular,
+    rewrite ↑rat_seq.regular,
     intro m n,
     apply le_of_rat_le_of_rat,
     rewrite [abs_const, -of_rat_sub, (rewrite_helper10 (X (Nb M m)) (X (Nb M n)))],
@@ -315,15 +294,15 @@ theorem lim_seq_reg : s.regular lim_seq :=
   end
 
 theorem lim_seq_spec (k : ℕ+) :
-        s.s_le (s.s_abs (s.sadd lim_seq (s.sneg (s.const (lim_seq k))))) (s.const k⁻¹) :=
-  by apply s.const_bound; apply lim_seq_reg
+        rat_seq.s_le (rat_seq.s_abs (rat_seq.sadd lim_seq (rat_seq.sneg (rat_seq.const (lim_seq k))))) (rat_seq.const k⁻¹) :=
+  by apply rat_seq.const_bound; apply lim_seq_reg
 
-noncomputable definition r_lim_seq : s.reg_seq :=
-  s.reg_seq.mk lim_seq lim_seq_reg
+private noncomputable definition r_lim_seq : rat_seq.reg_seq :=
+  rat_seq.reg_seq.mk lim_seq lim_seq_reg
 
-theorem r_lim_seq_spec (k : ℕ+) : s.r_le
-        (s.r_abs ((s.radd r_lim_seq (s.rneg (s.r_const ((s.reg_seq.sq r_lim_seq) k))))))
-        (s.r_const k⁻¹) :=
+private theorem r_lim_seq_spec (k : ℕ+) : rat_seq.r_le
+        (rat_seq.r_abs ((rat_seq.radd r_lim_seq (rat_seq.rneg (rat_seq.r_const ((rat_seq.reg_seq.sq r_lim_seq) k))))))
+        (rat_seq.r_const k⁻¹) :=
   lim_seq_spec k
 
 noncomputable definition lim : ℝ :=
@@ -384,7 +363,7 @@ theorem converges_of_cauchy : converges_to X lim (Nb M) :=
     apply Hn,
     rotate_right 1,
     apply Nb_spec_left,
-    rewrite [-*pnat.mul.assoc, p_add_fractions],
+    rewrite [-*pnat.mul.assoc, pnat.p_add_fractions],
     apply rat.le.refl
   end
 
@@ -396,15 +375,15 @@ section ints
 
 open int
 
-theorem archimedean (x : ℝ) : ∃ z : ℤ, x ≤ of_rat (of_int z) :=
+theorem archimedean_upper (x : ℝ) : ∃ z : ℤ, x ≤ of_rat (of_int z) :=
   begin
     apply quot.induction_on x,
     intro s,
-    cases s.bdd_of_regular (s.reg_seq.is_reg s) with [b, Hb],
+    cases rat_seq.bdd_of_regular (rat_seq.reg_seq.is_reg s) with [b, Hb],
     existsi ubound b,
-    have H : s.s_le (s.reg_seq.sq s) (s.const (rat.of_nat (ubound b))), begin
-      apply s.s_le_of_le_pointwise (s.reg_seq.is_reg s),
-      apply s.const_reg,
+    have H : rat_seq.s_le (rat_seq.reg_seq.sq s) (rat_seq.const (rat.of_nat (ubound b))), begin
+      apply rat_seq.s_le_of_le_pointwise (rat_seq.reg_seq.is_reg s),
+      apply rat_seq.const_reg,
       intro n,
       apply rat.le.trans,
       apply Hb,
@@ -413,9 +392,9 @@ theorem archimedean (x : ℝ) : ∃ z : ℤ, x ≤ of_rat (of_int z) :=
     apply H
   end
 
-theorem archimedean_strict (x : ℝ) : ∃ z : ℤ, x < of_rat (of_int z) :=
+theorem archimedean_upper_strict (x : ℝ) : ∃ z : ℤ, x < of_rat (of_int z) :=
   begin
-    cases archimedean x with [z, Hz],
+    cases archimedean_upper x with [z, Hz],
     existsi z + 1,
     apply lt_of_le_of_lt,
     apply Hz,
@@ -425,113 +404,39 @@ theorem archimedean_strict (x : ℝ) : ∃ z : ℤ, x < of_rat (of_int z) :=
     apply dec_trivial
   end
 
-theorem archimedean' (x : ℝ) : ∃ z : ℤ, x ≥ of_rat (of_int z) :=
+theorem archimedean_lower (x : ℝ) : ∃ z : ℤ, x ≥ of_rat (of_int z) :=
   begin
-    cases archimedean (-x) with [z, Hz],
+    cases archimedean_upper (-x) with [z, Hz],
     existsi -z,
     rewrite [of_int_neg, of_rat_neg],
     apply iff.mp !neg_le_iff_neg_le Hz
   end
 
-theorem archimedean_strict' (x : ℝ) : ∃ z : ℤ, x > of_rat (of_int z) :=
+theorem archimedean_lower_strict (x : ℝ) : ∃ z : ℤ, x > of_rat (of_int z) :=
   begin
-    cases archimedean_strict (-x) with [z, Hz],
+    cases archimedean_upper_strict (-x) with [z, Hz],
     existsi -z,
     rewrite [of_int_neg, of_rat_neg],
     apply iff.mp !neg_lt_iff_neg_lt Hz
   end
 
-theorem ex_smallest_of_bdd {P : ℤ → Prop} (Hbdd : ∃ b : ℤ, ∀ z : ℤ, z ≤ b → ¬ P z)
-        (Hinh : ∃ z : ℤ, P z) : ∃ lb : ℤ, P lb ∧ (∀ z : ℤ, z < lb → ¬ P z) :=
-  begin
-    cases Hbdd with [b, Hb],
-    cases Hinh with [elt, Helt],
-    existsi b + of_nat (least (λ n, P (b + of_nat n)) (succ (nat_abs (elt - b)))),
-    have Heltb : elt > b, begin
-      apply int.lt_of_not_ge,
-      intro Hge,
-      apply (Hb _ Hge) Helt
-    end,
-    have H' : P (b + of_nat (nat_abs (elt - b))), begin
-      rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !int.sub_pos_iff_lt Heltb)),
-              int.add.comm, int.sub_add_cancel],
-      apply Helt
-    end,
-    apply and.intro,
-    apply least_of_lt _ !lt_succ_self H',
-    intros z Hz,
-    cases em (z ≤ b) with [Hzb, Hzb],
-    apply Hb _ Hzb,
-    let Hzb' := int.lt_of_not_ge Hzb,
-    let Hpos := iff.mpr !int.sub_pos_iff_lt Hzb',
-    have Hzbk : z = b + of_nat (nat_abs (z - b)),
-      by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.add.comm, int.sub_add_cancel],
-    have Hk : nat_abs (z - b) < least (λ n, P (b + of_nat n)) (succ (nat_abs (elt - b))), begin
-     let Hz' := iff.mp !int.lt_add_iff_sub_lt_left Hz,
-     rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'],
-     apply iff.mp !int.of_nat_lt_of_nat Hz'
-    end,
-    let Hk' := nat.not_le_of_gt Hk,
-    rewrite Hzbk,
-    apply λ p, mt (ge_least_of_lt _ p) Hk',
-    apply nat.lt.trans Hk,
-    apply least_lt _ !lt_succ_self H'
-  end
-
-theorem ex_largest_of_bdd {P : ℤ → Prop} (Hbdd : ∃ b : ℤ, ∀ z : ℤ, z ≥ b → ¬ P z)
-        (Hinh : ∃ z : ℤ, P z) : ∃ ub : ℤ, P ub ∧ (∀ z : ℤ, z > ub → ¬ P z) :=
-  begin
-    cases Hbdd with [b, Hb],
-    cases Hinh with [elt, Helt],
-    existsi b - of_nat (least (λ n, P (b - of_nat n)) (succ (nat_abs (b - elt)))),
-    have Heltb : elt < b, begin
-      apply int.lt_of_not_ge,
-      intro Hge,
-      apply (Hb _ Hge) Helt
-    end,
-    have H' : P (b - of_nat (nat_abs (b - elt))), begin
-      rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !int.sub_pos_iff_lt Heltb)),
-              int.sub_sub_self],
-      apply Helt
-    end,
-    apply and.intro,
-    apply least_of_lt _ !lt_succ_self H',
-    intros z Hz,
-    cases em (z ≥ b) with [Hzb, Hzb],
-    apply Hb _ Hzb,
-    let Hzb' := int.lt_of_not_ge Hzb,
-    let Hpos := iff.mpr !int.sub_pos_iff_lt Hzb',
-    have Hzbk : z = b - of_nat (nat_abs (b - z)),
-      by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.sub_sub_self],
-    have Hk : nat_abs (b - z) < least (λ n, P (b - of_nat n)) (succ (nat_abs (b - elt))), begin
-      let Hz' := iff.mp !int.lt_add_iff_sub_lt_left (iff.mpr !int.lt_add_iff_sub_lt_right Hz),
-      rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'],
-      apply iff.mp !int.of_nat_lt_of_nat Hz'
-    end,
-    let Hk' := nat.not_le_of_gt Hk,
-    rewrite Hzbk,
-    apply λ p, mt (ge_least_of_lt _ p) Hk',
-    apply nat.lt.trans Hk,
-    apply least_lt _ !lt_succ_self H'
-  end
-
 definition ex_floor (x : ℝ) :=
-  (@ex_largest_of_bdd (λ z, x ≥ of_rat (of_int z))
+  (@ex_largest_of_bdd (λ z, x ≥ of_rat (of_int z)) _
     (begin
-      existsi some (archimedean_strict x),
-      let Har := some_spec (archimedean_strict x),
+      existsi some (archimedean_upper_strict x),
+      let Har := some_spec (archimedean_upper_strict x),
       intros z Hz,
       apply not_le_of_gt,
       apply lt_of_lt_of_le,
       apply Har,
-      have H : of_rat (of_int (some (archimedean_strict x))) ≤ of_rat (of_int z), begin
+      have H : of_rat (of_int (some (archimedean_upper_strict x))) ≤ of_rat (of_int z), begin
         apply of_rat_le_of_rat_of_le,
         apply iff.mpr !of_int_le_of_int,
         apply Hz
       end,
       exact H
     end)
-    (by existsi some (archimedean' x); apply some_spec (archimedean' x)))
+    (by existsi some (archimedean_lower x); apply some_spec (archimedean_lower x)))
 
 noncomputable definition floor (x : ℝ) : ℤ :=
   some (ex_floor x)
@@ -920,7 +825,7 @@ theorem over_seq_mono (i j : ℕ) (H : i ≤ j) : over_seq j ≤ over_seq i :=
 theorem rat_power_two_inv_ge (k : ℕ+) : 1 / rat.pow 2 k~ ≤ k⁻¹ :=
   rat.div_le_div_of_le !rat_of_pnat_is_pos !rat_power_two_le
 
-open s
+open rat_seq
 theorem regular_lemma_helper {s : seq} {m n : ℕ+} (Hm : m ≤ n)
         (H : ∀ n i : ℕ+, i ≥ n → under_seq' n~ ≤ s i ∧ s i ≤ over_seq' n~) :
         rat.abs (s m - s n) ≤ m⁻¹ + n⁻¹ :=

library/data/real/division.lean

@@ -17,13 +17,7 @@ local notation 0 := rat.of_num 0
 local notation 1 := rat.of_num 1
 local notation 2 := subtype.tag (nat.of_num 2) dec_trivial
 
-namespace s
-
------------------------------
--- helper lemmas
-
-theorem and_of_not_or {a b : Prop} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b :=
-  and.intro (assume H', H (or.inl H')) (assume H', H (or.inr H'))
+namespace rat_seq
 
 -----------------------------
 -- Facts about absolute values of sequences, to define inverse
@@ -70,6 +64,17 @@ theorem abs_pos_of_nonzero {s : seq} (Hs : regular s) (Hnz : sep s zero) :
     apply le_abs_self
   end
 
+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 sep_zero_of_pos {s : seq} (Hs : regular s) (Hpos : pos s) : sep s zero :=
   begin
     apply or.inr,
@@ -84,17 +89,17 @@ theorem sep_zero_of_pos {s : seq} (Hs : regular s) (Hpos : pos s) : sep s zero :
 ------------------------
 -- This section could be cleaned up.
 
-noncomputable definition pb {s : seq} (Hs : regular s) (Hpos : pos s) :=
+private noncomputable definition pb {s : seq} (Hs : regular s) (Hpos : pos s) :=
   some (abs_pos_of_nonzero Hs (sep_zero_of_pos Hs Hpos))
-noncomputable definition ps {s : seq} (Hs : regular s) (Hsep : sep s zero) :=
+private noncomputable definition ps {s : seq} (Hs : regular s) (Hsep : sep s zero) :=
   some (abs_pos_of_nonzero Hs Hsep)
 
 
-theorem pb_spec {s : seq} (Hs : regular s) (Hpos : pos s) :
+private theorem pb_spec {s : seq} (Hs : regular s) (Hpos : pos s) :
         ∀ m : ℕ+, m ≥ (pb Hs Hpos) → abs (s m) ≥ (pb Hs Hpos)⁻¹ :=
   some_spec (abs_pos_of_nonzero Hs (sep_zero_of_pos Hs Hpos))
 
-theorem ps_spec {s : seq} (Hs : regular s) (Hsep : sep s zero) :
+private theorem ps_spec {s : seq} (Hs : regular s) (Hsep : sep s zero) :
         ∀ m : ℕ+, m ≥ (ps Hs Hsep) → abs (s m) ≥ (ps Hs Hsep)⁻¹ :=
   some_spec (abs_pos_of_nonzero Hs Hsep)
 
@@ -104,11 +109,10 @@ noncomputable definition s_inv {s : seq} (Hs : regular s) (n : ℕ+) : ℚ :=
         else 1 / (s ((ps Hs H) * (ps Hs H) * n)))
   else 0
 
-theorem peq {s : seq} (Hsep : sep s zero) (Hpos : pos s)  (Hs : regular s) :
+private theorem peq {s : seq} (Hsep : sep s zero) (Hpos : pos s)  (Hs : regular s) :
         pb Hs Hpos = ps Hs Hsep := rfl
 
-
-theorem s_inv_of_sep_lt_p {s : seq} (Hs : regular s) (Hsep : sep s zero) {n : ℕ+}
+private theorem s_inv_of_sep_lt_p {s : seq} (Hs : regular s) (Hsep : sep s zero) {n : ℕ+}
         (Hn : n < (ps Hs Hsep)) : s_inv Hs n = 1 / s ((ps Hs Hsep) * (ps Hs Hsep) * (ps Hs Hsep)) :=
   begin
     apply eq.trans,
@@ -116,7 +120,7 @@ theorem s_inv_of_sep_lt_p {s : seq} (Hs : regular s) (Hsep : sep s zero) {n :
     apply dif_pos Hn
   end
 
-theorem s_inv_of_sep_gt_p {s : seq} (Hs : regular s) (Hsep : sep s zero) {n : ℕ+}
+private theorem s_inv_of_sep_gt_p {s : seq} (Hs : regular s) (Hsep : sep s zero) {n : ℕ+}
         (Hn : n ≥ (ps Hs Hsep)) : s_inv Hs n = 1 / s ((ps Hs Hsep) * (ps Hs Hsep) * n) :=
   begin
     apply eq.trans,
@@ -124,16 +128,15 @@ theorem s_inv_of_sep_gt_p {s : seq} (Hs : regular s) (Hsep : sep s zero) {n :
     apply dif_neg (pnat.not_lt_of_ge Hn)
   end
 
-theorem s_inv_of_pos_lt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+}
+private theorem s_inv_of_pos_lt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+}
         (Hn : n < (pb Hs Hpos)) : s_inv Hs n = 1 / s ((pb Hs Hpos) * (pb Hs Hpos) * (pb Hs Hpos)) :=
   s_inv_of_sep_lt_p Hs (sep_zero_of_pos Hs Hpos) Hn
 
-
-theorem s_inv_of_pos_gt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+}
+private theorem s_inv_of_pos_gt_p {s : seq} (Hs : regular s) (Hpos : pos s) {n : ℕ+}
         (Hn : n ≥ (pb Hs Hpos)) : s_inv Hs n = 1 / s ((pb Hs Hpos) * (pb Hs Hpos) * n) :=
   s_inv_of_sep_gt_p Hs (sep_zero_of_pos Hs Hpos) Hn
 
-theorem le_ps {s : seq} (Hs : regular s) (Hsep : sep s zero) (n : ℕ+) :
+private theorem le_ps {s : seq} (Hs : regular s) (Hsep : sep s zero) (n : ℕ+) :
         abs (s_inv Hs n) ≤ (rat_of_pnat (ps Hs Hsep)) :=
   if Hn : n < ps Hs Hsep then
     (begin
@@ -154,7 +157,7 @@ theorem le_ps {s : seq} (Hs : regular s) (Hsep : sep s zero) (n : ℕ+) :
 theorem s_inv_zero : s_inv zero_is_reg = zero :=
   funext (λ n, dif_neg (!not_sep_self))
 
-theorem s_inv_of_zero' {s : seq} (Hs : regular s) (Hz : ¬ sep s zero) (n : ℕ+) : s_inv Hs n = 0 :=
+private theorem s_inv_of_zero' {s : seq} (Hs : regular s) (Hz : ¬ sep s zero) (n : ℕ+) : s_inv Hs n = 0 :=
   dif_neg Hz
 
 theorem s_inv_of_zero {s : seq} (Hs : regular s) (Hz : ¬ sep s zero) : s_inv Hs = zero :=
@@ -164,7 +167,7 @@ theorem s_inv_of_zero {s : seq} (Hs : regular s) (Hz : ¬ sep s zero) : s_inv Hs
     apply s_inv_of_zero' Hs Hz n
   end
 
-theorem s_ne_zero_of_ge_p {s : seq} (Hs : regular s) (Hsep : sep s zero) {n : ℕ+}
+private theorem s_ne_zero_of_ge_p {s : seq} (Hs : regular s) (Hsep : sep s zero) {n : ℕ+}
         (Hn : n ≥ (ps Hs Hsep)) : s n ≠ 0 :=
   begin
     let Hps := ps_spec Hs Hsep,
@@ -498,7 +501,7 @@ theorem sep_of_nequiv {s t : seq} (Hs : regular s) (Ht : regular t) (Hneq : ¬ e
     rewrite ↑sep,
     apply by_contradiction,
     intro Hnor,
-    let Hand := and_of_not_or Hnor,
+    let Hand := iff.mp !not_or_iff_not_and_not Hnor,
     let Hle1 := s_le_of_not_lt (and.left Hand),
     let Hle2 := s_le_of_not_lt (and.right Hand),
     apply Hneq (equiv_of_le_of_ge Hs Ht Hle2 Hle1)
@@ -570,21 +573,26 @@ theorem r_le_of_equiv_le_left {s t u : reg_seq} (Heq : requiv s t) (Hle : r_le s
 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
+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 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
+
+end rat_seq
 
 namespace real
-open [classes] s
+open [classes] rat_seq
 
-noncomputable definition inv (x : ℝ) : ℝ := quot.lift_on x (λ a, quot.mk (s.r_inv a))
-           (λ a b H, quot.sound (s.r_inv_well_defined H))
+noncomputable definition inv (x : ℝ) : ℝ := quot.lift_on x (λ a, quot.mk (rat_seq.r_inv a))
+           (λ a b H, quot.sound (rat_seq.r_inv_well_defined H))
 postfix [priority real.prio] `⁻¹` := inv
 
 theorem le_total (x y : ℝ) : x ≤ y ∨ y ≤ x :=
-  quot.induction_on₂ x y (λ s t, s.r_le_total s t)
+  quot.induction_on₂ x y (λ s t, rat_seq.r_le_total s t)
 
 theorem mul_inv' (x : ℝ) : x ≢ 0 → x * x⁻¹ = 1 :=
-  quot.induction_on x (λ s H, quot.sound (s.r_mul_inv s H))
+  quot.induction_on x (λ s H, quot.sound (rat_seq.r_mul_inv s H))
 
 theorem inv_mul' (x : ℝ) : x ≢ 0 → x⁻¹ * x = 1 :=
   by rewrite real.mul_comm; apply mul_inv'
@@ -593,7 +601,7 @@ theorem neq_of_sep {x y : ℝ} (H : x ≢ y) : ¬ x = y :=
   assume Heq, !not_sep_self (Heq ▸ H)
 
 theorem sep_of_neq {x y : ℝ} : ¬ x = y → x ≢ y :=
-  quot.induction_on₂ x y (λ s t H, s.r_sep_of_nequiv s t (assume Heq, H (quot.sound Heq)))
+  quot.induction_on₂ x y (λ s t H, rat_seq.r_sep_of_nequiv s t (assume Heq, H (quot.sound Heq)))
 
 theorem sep_is_neq (x y : ℝ) : (x ≢ y) = (¬ x = y) :=
   propext (iff.intro neq_of_sep sep_of_neq)
@@ -602,10 +610,10 @@ theorem mul_inv (x : ℝ) : x ≠ 0 → x * x⁻¹ = 1 := !sep_is_neq ▸ !mul_i
 
 theorem inv_mul (x : ℝ) : x ≠ 0 → x⁻¹ * x = 1 := !sep_is_neq ▸ !inv_mul'
 
-theorem inv_zero : (0 : ℝ)⁻¹ = 0 := quot.sound (s.r_inv_zero)
+theorem inv_zero : (0 : ℝ)⁻¹ = 0 := quot.sound (rat_seq.r_inv_zero)
 
 theorem lt_or_eq_of_le (x y : ℝ) : x ≤ y → x < y ∨ x = y :=
-  quot.induction_on₂ x y (λ s t H, or.elim (s.r_lt_or_equiv_of_le s t H)
+  quot.induction_on₂ x y (λ s t H, or.elim (rat_seq.r_lt_or_equiv_of_le s t H)
     (assume H1, or.inl H1)
     (assume H2, or.inr (quot.sound H2)))
 

library/data/real/order.lean

@@ -16,7 +16,7 @@ local notation 0 := rat.of_num 0
 local notation 1 := rat.of_num 1
 local notation 2 := subtype.tag (of_num 2) dec_trivial
 
-namespace s
+namespace rat_seq
 definition pos (s : seq) := ∃ n : ℕ+, n⁻¹ < (s n)
 
 definition nonneg (s : seq) := ∀ n : ℕ+, -(n⁻¹) ≤ s n
@@ -76,7 +76,7 @@ theorem nonneg_of_bdd_within {s : seq} (Hs : regular s)
   begin
     rewrite ↑nonneg,
     intro k,
-    apply squeeze_2,
+    apply ge_of_forall_ge_sub,
     intro ε Hε,
     cases H (pceil ((1 + 1) / ε)) with [N, HN],
     apply le.trans,
@@ -907,7 +907,7 @@ theorem lt_of_const_lt_const {a b : ℚ} (H : s_lt (const a) (const b)) : a < b
     apply pnat.inv_pos
   end
 
-theorem s_le_of_le_pointwise {s t : seq} (Hs : regular s) (Ht : s.regular t)
+theorem s_le_of_le_pointwise {s t : seq} (Hs : regular s) (Ht : regular t)
         (H : ∀ n : ℕ+, s n ≤ t n) : s_le s t :=
   begin
     rewrite [↑s_le, ↑nonneg, ↑sadd, ↑sneg],
@@ -1013,16 +1013,16 @@ theorem r_le_of_le_reprs (s t : reg_seq) (Hle : ∀ n : ℕ+, r_le s (r_const (r
 theorem r_le_of_reprs_le (s t : reg_seq) (Hle : ∀ n : ℕ+, r_le (r_const (reg_seq.sq t n)) s) : r_le t s :=
   le_of_reprs_le (reg_seq.is_reg s) (reg_seq.is_reg t) Hle
 
-end s
+end rat_seq
 
 open real
-open [classes] s
+open [classes] rat_seq
 namespace real
 
-definition lt (x y : ℝ) := quot.lift_on₂ x y (λ a b, s.r_lt a b) s.r_lt_well_defined
+definition lt (x y : ℝ) := quot.lift_on₂ x y (λ a b, rat_seq.r_lt a b) rat_seq.r_lt_well_defined
 infix [priority real.prio] `<` := lt
 
-definition le (x y : ℝ) := quot.lift_on₂ x y (λ a b, s.r_le a b) s.r_le_well_defined
+definition le (x y : ℝ) := quot.lift_on₂ x y (λ a b, rat_seq.r_le a b) rat_seq.r_le_well_defined
 infix [priority real.prio] `<=` := le
 infix [priority real.prio] `≤` := le
 
@@ -1033,63 +1033,63 @@ infix [priority real.prio] >= := real.ge
 infix [priority real.prio] ≥  := real.ge
 infix [priority real.prio] >  := real.gt
 
-definition sep (x y : ℝ) := quot.lift_on₂ x y (λ a b, s.r_sep a b) s.r_sep_well_defined
+definition sep (x y : ℝ) := quot.lift_on₂ x y (λ a b, rat_seq.r_sep a b) rat_seq.r_sep_well_defined
 infix `≢` : 50 := sep
 
 theorem le.refl (x : ℝ) : x ≤ x :=
-  quot.induction_on x (λ t, s.r_le.refl t)
+  quot.induction_on x (λ t, rat_seq.r_le.refl t)
 
-theorem le.trans (x y z : ℝ) : x ≤ y → y ≤ z → x ≤ z :=
-  quot.induction_on₃ x y z (λ s t u, s.r_le.trans)
+theorem le.trans {x y z : ℝ} : x ≤ y → y ≤ z → x ≤ z :=
+  quot.induction_on₃ x y z (λ s t u, rat_seq.r_le.trans)
 
-theorem eq_of_le_of_ge (x y : ℝ) : x ≤ y → y ≤ x → x = y :=
-  quot.induction_on₂ x y (λ s t Hst Hts, quot.sound (s.r_equiv_of_le_of_ge Hst Hts))
+theorem eq_of_le_of_ge {x y : ℝ} : x ≤ y → y ≤ x → x = y :=
+  quot.induction_on₂ x y (λ s t Hst Hts, quot.sound (rat_seq.r_equiv_of_le_of_ge Hst Hts))
 
 theorem lt_iff_le_and_sep (x y : ℝ) : x < y ↔ x ≤ y ∧ x ≢ y :=
-  quot.induction_on₂ x y (λ s t, s.r_lt_iff_le_and_sep s t)
+  quot.induction_on₂ x y (λ s t, rat_seq.r_lt_iff_le_and_sep s t)
 
 theorem add_le_add_of_le_right_var (x y z : ℝ) : x ≤ y → z + x ≤ z + y :=
-  quot.induction_on₃ x y z (λ s t u, s.r_add_le_add_of_le_right_var s t u)
+  quot.induction_on₃ x y z (λ s t u, rat_seq.r_add_le_add_of_le_right_var s t u)
 
 theorem add_le_add_of_le_right (x y : ℝ) : x ≤ y → ∀ z : ℝ, z + x ≤ z + y :=
   take H z, add_le_add_of_le_right_var x y z H
 
 theorem mul_gt_zero_of_gt_zero (x y : ℝ) : zero < x → zero < y → zero < x * y :=
-  quot.induction_on₂ x y (λ s t, s.r_mul_pos_of_pos)
+  quot.induction_on₂ x y (λ s t, rat_seq.r_mul_pos_of_pos)
 
 theorem mul_ge_zero_of_ge_zero (x y : ℝ) : zero ≤ x → zero ≤ y → zero ≤ x * y :=
-  quot.induction_on₂ x y (λ s t, s.r_mul_nonneg_of_nonneg)
+  quot.induction_on₂ x y (λ s t, rat_seq.r_mul_nonneg_of_nonneg)
 
 theorem not_sep_self (x : ℝ) : ¬ x ≢ x :=
-  quot.induction_on x (λ s, s.r_not_sep_self s)
+  quot.induction_on x (λ s, rat_seq.r_not_sep_self s)
 
 theorem not_lt_self (x : ℝ) : ¬ x < x :=
-  quot.induction_on x (λ s, s.r_not_lt_self s)
+  quot.induction_on x (λ s, rat_seq.r_not_lt_self s)
 
 theorem le_of_lt {x y : ℝ} : x < y → x ≤ y :=
-  quot.induction_on₂ x y (λ s t H', s.r_le_of_lt H')
+  quot.induction_on₂ x y (λ s t H', rat_seq.r_le_of_lt H')
 
 theorem lt_of_le_of_lt {x y z : ℝ} : x ≤ y → y < z → x < z :=
-  quot.induction_on₃ x y z (λ s t u H H', s.r_lt_of_le_of_lt H H')
+  quot.induction_on₃ x y z (λ s t u H H', rat_seq.r_lt_of_le_of_lt H H')
 
 theorem lt_of_lt_of_le {x y z : ℝ} : x < y → y ≤ z → x < z :=
-  quot.induction_on₃ x y z (λ s t u H H', s.r_lt_of_lt_of_le H H')
+  quot.induction_on₃ x y z (λ s t u H H', rat_seq.r_lt_of_lt_of_le H H')
 
 theorem add_lt_add_left_var (x y z : ℝ) : x < y → z + x < z + y :=
-  quot.induction_on₃ x y z (λ s t u, s.r_add_lt_add_left_var s t u)
+  quot.induction_on₃ x y z (λ s t u, rat_seq.r_add_lt_add_left_var s t u)
 
 theorem add_lt_add_left (x y : ℝ) : x < y → ∀ z : ℝ, z + x < z + y :=
   take H z, add_lt_add_left_var x y z H
 
-theorem zero_lt_one : (0 : ℝ) < (1 : ℝ) := s.r_zero_lt_one
+theorem zero_lt_one : (0 : ℝ) < (1 : ℝ) := rat_seq.r_zero_lt_one
 
 theorem le_of_lt_or_eq (x y : ℝ) : x < y ∨ x = y → x ≤ y :=
     (quot.induction_on₂ x y (λ s t H, or.elim H (take H', begin
-        apply s.r_le_of_lt_or_eq,
+        apply rat_seq.r_le_of_lt_or_eq,
         apply or.inl H'
       end)
       (take H', begin
-        apply s.r_le_of_lt_or_eq,
+        apply rat_seq.r_le_of_lt_or_eq,
         apply (or.inr (quot.exact H'))
       end)))
 
@@ -1099,12 +1099,12 @@ section migrate_algebra
   protected definition ordered_ring [reducible]  : algebra.ordered_ring ℝ :=
   ⦃ algebra.ordered_ring, real.comm_ring,
     le_refl := le.refl,
-    le_trans := le.trans,
+    le_trans := @le.trans,
     mul_pos := mul_gt_zero_of_gt_zero,
     mul_nonneg := mul_ge_zero_of_ge_zero,
     zero_ne_one := zero_ne_one,
     add_le_add_left := add_le_add_of_le_right,
-    le_antisymm := eq_of_le_of_ge,
+    le_antisymm := @eq_of_le_of_ge,
     lt_irrefl := not_lt_self,
     lt_of_le_of_lt := @lt_of_le_of_lt,
     lt_of_lt_of_le := @lt_of_lt_of_le,
@@ -1134,24 +1134,24 @@ section migrate_algebra
 end migrate_algebra
 
 theorem of_rat_le_of_rat_of_le (a b : ℚ) : a ≤ b → of_rat a ≤ of_rat b :=
-  s.r_const_le_const_of_le
+  rat_seq.r_const_le_const_of_le
 
 theorem le_of_rat_le_of_rat (a b : ℚ) : of_rat a ≤ of_rat b → a ≤ b :=
-  s.r_le_of_const_le_const
+  rat_seq.r_le_of_const_le_const
 
 theorem of_rat_lt_of_rat_of_lt (a b : ℚ) : a < b → of_rat a < of_rat b :=
-  s.r_const_lt_const_of_lt
+  rat_seq.r_const_lt_const_of_lt
 
 theorem lt_of_rat_lt_of_rat (a b : ℚ) : of_rat a < of_rat b → a < b :=
-  s.r_lt_of_const_lt_const
+  rat_seq.r_lt_of_const_lt_const
 
 theorem of_rat_sub (a b : ℚ) : of_rat a - of_rat b = of_rat (a - b) := rfl
 
-open s
+open rat_seq
 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,
-    show s.r_le s (reg_seq.mk t Ht), from
+    show r_le s (reg_seq.mk t Ht), from
       have H' : ∀ n : ℕ+, r_le s (r_const (t n)), from Hs,
       by apply r_le_of_le_reprs; apply Hs)
 
@@ -1159,7 +1159,7 @@ theorem le_of_le_reprs (x : ℝ) (t : seq) (Ht : regular t) : (∀ n : ℕ+, x
 theorem le_of_reprs_le (x : ℝ) (t : seq) (Ht : regular t) : (∀ n : ℕ+, t n ≤ x) →
         quot.mk (reg_seq.mk t Ht) ≤ x :=
   quot.induction_on x (take s Hs,
-    show s.r_le (reg_seq.mk t Ht) s, from
+    show r_le (reg_seq.mk t Ht) s, from
       have H' : ∀ n : ℕ+, r_le (r_const (t n)) s, from Hs,
       by apply r_le_of_reprs_le; apply Hs)