From cf7c85e5fdd424850b45e2912c983915d6265f5a Mon Sep 17 00:00:00 2001
From: Rob Lewis <rlewis1@andrew.cmu.edu>
Date: Thu, 11 Jun 2015 17:01:55 +1000
Subject: [PATCH] feat(library/data/real): fill in lots of sorrys about pnats

---
 library/data/real/basic.lean    | 13 ++++++++-----
 library/data/real/complete.lean |  2 ++
 library/data/real/division.lean |  5 +----
 library/data/real/order.lean    |  5 +----
 4 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index 53f32d2dd..fb3b938c4 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -11,8 +11,8 @@ To do:
  o Rename things and possibly make theorems private
 -/
 
-import data.nat data.rat.order
-open nat eq eq.ops
+import data.nat data.rat.order data.nat.pnat
+open nat eq eq.ops pnat
 open -[coercions] rat
 local notation 0 := rat.of_num 0
 local notation 1 := rat.of_num 1
@@ -21,7 +21,7 @@ local notation 1 := rat.of_num 1
 -----------------------------------------------
 -- positive naturals
 
-inductive pnat : Type :=
+/-inductive pnat : Type :=
   pos : Π n : nat, n > 0 → pnat
 
 notation `ℕ+` := pnat
@@ -169,7 +169,7 @@ theorem pnat.lt_of_not_le {p q : ℕ+} (H : ¬ p ≤ q) : q < p := sorry
 
 theorem pnat.inv_cancel (p : ℕ+) : pnat.to_rat p * p⁻¹ = (1 : ℚ) := sorry
 
-theorem pnat.inv_cancel_right (p : ℕ+) : p⁻¹ * pnat.to_rat p = (1 : ℚ) := sorry
+theorem pnat.inv_cancel_right (p : ℕ+) : p⁻¹ * pnat.to_rat p = (1 : ℚ) := sorry-/
 
 -------------------------------------
 -- theorems to add to (ordered) field and/or rat
@@ -220,6 +220,9 @@ theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq : q > 0)
 -------------------------------------
 -- small helper lemmas
 
+theorem s_mul_assoc_lemma_3 (a b n : ℕ+) (p : ℚ) :
+        p * ((a * n)⁻¹ + (b * n)⁻¹) = p * (a⁻¹ + b⁻¹) * n⁻¹ := sorry
+
 theorem find_thirds (a b : ℚ) : ∃ n : ℕ+, a + n⁻¹ + n⁻¹ + n⁻¹ < a + b := sorry
 
 theorem squeeze {a b : ℚ} (H : ∀ j : ℕ+, a ≤ b + j⁻¹ + j⁻¹ + j⁻¹) : a ≤ b :=
@@ -1073,7 +1076,7 @@ theorem zero_nequiv_one : ¬ zero ≡ one :=
       ... = abs 1 : abs_of_pos zero_lt_one
       ... ≤ 2⁻¹ : H,
     let H'' := ge_of_inv_le H',
-    apply absurd (one_lt_two) (pnat.not_lt_of_le (pnat.le_of_lt H''))
+    apply absurd (one_lt_two) (pnat.not_lt_of_le H'')
   end
 
 ---------------------------------------------
diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean
index 78ead4b03..62275df34 100644
--- a/library/data/real/complete.lean
+++ b/library/data/real/complete.lean
@@ -237,6 +237,8 @@ end s
 
 namespace real
 
+theorem p_add_fractions (n : ℕ+) : (2 * n)⁻¹ + (2 * 3 * n)⁻¹ + (3 * n)⁻¹ = n⁻¹ := sorry
+
 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
diff --git a/library/data/real/division.lean b/library/data/real/division.lean
index a52003ed3..a2c5444d3 100644
--- a/library/data/real/division.lean
+++ b/library/data/real/division.lean
@@ -14,7 +14,7 @@ open -[coercions] rat
 open -[coercions] nat
 local notation 0 := rat.of_num 0
 local notation 1 := rat.of_num 1
-open eq.ops
+open eq.ops pnat
 
 
 local notation 2 := pnat.pos (nat.of_num 2) dec_trivial
@@ -44,9 +44,6 @@ theorem abs_abs_sub_abs_le_abs_sub (a b : ℚ) : abs (abs a - abs b) ≤ abs (a
 
 theorem abs_one_div (q : ℚ) : abs (1 / q) = 1 / abs q := sorry
 
-theorem div_le_pnat (q : ℚ) (n : ℕ+) (H : q ≥ n⁻¹) : 1 / q ≤ pnat.to_rat n := sorry
-
-theorem pnat_cancel' (n m : ℕ+) : (n * n * m)⁻¹ * (pnat.to_rat n * pnat.to_rat n) = m⁻¹ := sorry
 
 -- does this not exist already??
 theorem forall_of_not_exists {A : Type} {P : A → Prop} (H : ¬ ∃ a : A, P a) : ∀ a : A, ¬ P a :=
diff --git a/library/data/real/order.lean b/library/data/real/order.lean
index 109e6392f..5b5184858 100644
--- a/library/data/real/order.lean
+++ b/library/data/real/order.lean
@@ -14,16 +14,13 @@ To do:
 import data.real.basic data.rat data.nat
 open -[coercions] rat
 open -[coercions] nat
-open eq eq.ops
+open eq eq.ops pnat
 local notation 0 := rat.of_num 0
 local notation 1 := rat.of_num 1
 
 ----------------------------------------------------------------------------------------------------
 
 -- pnat theorems
-theorem inv_add_lt_left (p q : ℕ+) : (p + q)⁻¹ < p⁻¹ := sorry
-
-theorem pnat_lt_add_left (p q : ℕ+) : p < p + q  := sorry
 
 notation 2 := pnat.pos (of_num 2) dec_trivial