...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

diff --git a/helm/software/matita/nlibrary/arithmetics/R.ma b/helm/software/matita/nlibrary/arithmetics/R.ma
index 813dec9fb1162617267a0ca1824e07db5a6b1a40..805a0a37fd0ea66bae50b7ef79d9c1210f061e9a 100644 (file)
--- a/helm/software/matita/nlibrary/arithmetics/R.ma
+++ b/helm/software/matita/nlibrary/arithmetics/R.ma
@@ -25,6 +25,8 @@ naxiom Qtimes: Q → Q → Q.
 naxiom Qdivides: Q → Q → Q.
 naxiom Qle : Q → Q → Prop.
 naxiom Qlt: Q → Q → Prop.
+naxiom Qmin: Q → Q → Q.
+naxiom Qmax: Q → Q → Q.
 interpretation "Q plus" 'plus x y = (Qplus x y).
 interpretation "Q minus" 'minus x y = (Qminus x y).
 interpretation "Q times" 'times x y = (Qtimes x y).
@@ -243,4 +245,17 @@ nrecord Pt (A: Ax_pro) : Type[1] ≝
    pt_inhabited: ∃a. a ∈ pt_set;
    pt_filtering: ∀a,b. a ∈ pt_set → b ∈ pt_set → ∃c. c ∈ (singleton … a) ↓ (singleton … b) → c ∈ pt_set;
    pt_closed: {b | b ⋉ pt_set} ⊆ pt_set   
- }.
\ No newline at end of file
+ }.
+
+ndefinition Rd ≝ Pt Rax.
+
+naxiom daemon: False.
+
+ndefinition Q_to_R: Q → Rd.
+ #q; @
+  [ napply { c | fst … c < q ∧ q < snd … c  }
+  | @ [ @ (Qminus q 1) (Qplus q 1) | ncases daemon ]
+##| #c; #d; #Hc; #Hd; @ [ @ (Qmin (fst … c) (fst … d)) (Qmax (snd … c) (snd … d)) | ncases daemon]
+##| #a; #H; nlapply (ftcoreflexivity … H); /2/ ]
+nqed.
+