nat model ported to the dualized version, but not itself dualized dedekind-sig-compl...

[helm.git] / helm / software / matita / contribs / dama / dama / models / nat_dedekind_sigma_complete.ma

diff --git a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
index 5cf875f80a1455fb3cc4aebac6838a3d5e195b83..9681b4d93618b6fc4ef7a66dd21796b2fe5d0b3e 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma
@@ -17,16 +17,22 @@ include "supremum.ma".
 include "nat/le_arith.ma".
 include "russell_support.ma".
 
+lemma hint1:
+ ∀l,u.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set l u))
+   → sequence (hos_carr (os_l (segment_ordered_set nat_ordered_set l u))).
+intros; assumption;
+qed.   
+   
+coercion hint1 nocomposites.   
+   
 alias symbol "pi1" = "exT \fst".
-alias symbol "leq" = "natural 'less or equal to'".
+alias symbol "N" = "ordered set N".
 lemma nat_dedekind_sigma_complete:
   ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → 
     ∀x.x is_supremum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
 intros 5; cases x (s Hs); clear x; letin X ≝ ≪s,Hs≫; 
 fold normalize X; intros; cases H1; 
-alias symbol "plus" = "natural plus".
-alias symbol "N" = "Uniform space N".
-alias symbol "and" = "logical and".
+alias symbol "N" = "Natural numbers".
 letin spec ≝ (λi,j:ℕ.(u≤i ∧ s = \fst (a j)) ∨ (i < u ∧ s+i ≤ u + \fst (a j))); 
 (* s - aj <= max 0 (u - i) *)  
 letin m ≝ (hide ? (
@@ -109,14 +115,21 @@ exists [apply w]; intros; change with (s = \fst (a j));
 rewrite > (H4 ?); [2: reflexivity]
 apply le_to_le_to_eq;
 [1: apply os_le_to_nat_le;
-    apply (trans_increasing ?? H ? ? (nat_le_to_os_le ?? H5));
+    apply (trans_increasing ? H ? ? (nat_le_to_os_le ?? H5));
 |2: apply (trans_le ? s ?);[apply os_le_to_nat_le; apply (H2 j);]
     rewrite < (H4 ?); [2: reflexivity] apply le_n;]
 qed.
 
-alias symbol "pi1" = "exT \fst".
-alias symbol "leq" = "natural 'less or equal to'".
+lemma hint2:
+ ∀l,u.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set l u))
+   → sequence (hos_carr (os_r (segment_ordered_set nat_ordered_set l u))).
+intros; assumption;
+qed.   
+   
+coercion hint2 nocomposites.   
+   
 alias symbol "N" = "ordered set N".
 axiom nat_dedekind_sigma_complete_r:
   ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_decreasing → 
     ∀x.x is_infimum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
+