From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 Apr 2010 14:06:35 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~2922
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dc677ddf8e3cf907479264060565aa3e04f65d59;p=helm.git

...

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 813dec9fb..805a0a37f 100644
--- 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.
+