...

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 805a0a37fd0ea66bae50b7ef79d9c1210f061e9a..60de71dbd7a2eb6d5fd69a6851603f2bb72dc060 100644 (file)
--- a/helm/software/matita/nlibrary/arithmetics/R.ma
+++ b/helm/software/matita/nlibrary/arithmetics/R.ma
@@ -44,6 +44,9 @@ ntheorem Qplus_assoc1: ∀q1,q2,q3. q1 + q2 + q3 = q3 + q2 + q1.
 #a; #b; #c; //; nqed.
 naxiom Qle_refl: ∀q1. q1≤q1.
 naxiom Qle_trans: ∀x,y,z. x≤y → y≤z → x≤z.
+naxiom Qlt_trans: ∀x,y,z. x < y → y < z → x < z.
+naxiom Qle_lt_trans1: ∀x,y,z. x ≤ y → y < z → x < z.
+naxiom Qle_lt_trans2: ∀x,y,z. x < y → y ≤ z → x < z.
 naxiom Qle_plus_compat: ∀x,y,z,t. x≤y → z≤t → x+z ≤ y+t.
 naxiom Qmult_zero: ∀q:Q. 0 * q = 0.
 
@@ -141,7 +144,7 @@ include "datatypes/sums.ma".
 
 nrecord pre_order (A: Type[0]) : Type[1] ≝
  { pre_r :2> A → A → CProp[0];
-   pre_sym: reflexive … pre_r;
+   pre_refl: reflexive … pre_r;
    pre_trans: transitive … pre_r
  }.
 
@@ -228,6 +231,23 @@ nlemma ftcoleqleft:
  #A; #F; #a; #H; ncases H; /2/.
 nqed.
 
+alias symbol "I" (instance 7) = "I".
+alias symbol "I" (instance 18) = "I".
+alias symbol "I" (instance 18) = "I".
+alias symbol "I" (instance 18) = "I".
+nlet corec ftfish_coind
+ (A: Ax_pro) (F: Ω^A) (P: A → CProp[0])
+ (Hcorefl: ∀a. P a → a ∈ F)
+ (Hcoleqleft: ∀a. P a → ∀b. a ≤ b → P b)
+ (Hcoleqinfinity: ∀a. P a → ∀b. a ≤ b → ∀i:𝐈 b. ∃x. x ∈ 𝐂 b i ↓ (singleton … a) ∧ P x)
+: ∀a:A. P a → a ⋉ F ≝ ?.
+ #a; #H; @
+  [ /2/
+  | #b; #H; napply (ftfish_coind … Hcorefl Hcoleqleft Hcoleqinfinity); /2/
+  | #b; #H1; #i; ncases (Hcoleqinfinity a H ? H1 i); #x; *; #H2; #H3;
+    @ x; @; //; napply (ftfish_coind … Hcorefl Hcoleqleft Hcoleqinfinity); //]
+nqed.
+
 (*CSC: non serve manco questo (vedi sotto) *)
 nlemma auto_hint3: ∀A. S__o__AAx A = S (AAx A).
  #A; //.
@@ -244,7 +264,7 @@ nrecord Pt (A: Ax_pro) : Type[1] ≝
  { pt_set: Ω^A;
    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   
+   pt_closed: pt_set ⊆ {b | b ⋉ pt_set}   
  }.
 
 ndefinition Rd ≝ Pt Rax.
@@ -256,6 +276,10 @@ ndefinition Q_to_R: Q → Rd.
   [ 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/ ]
+##| #a; #H; napply (ftfish_coind Rax ? (λa. fst … a < q ∧ q < snd … a)); /2/
+    [ /5/ | #b; *; #H1; #H2; #c; *; #H3; #H4; #i; ncases i
+      [ #w; nnormalize;
+    ##| nnormalize;
+  ]
 nqed.