X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fnat_order_continuous.ma;h=5f00dc338d217a855296d51c18985d6f7174467e;hb=a6f88a0acfcb5c5284b7b3781e313cc0f76bb76d;hp=0b4c92e3e9f67fe5bd8f04ea629ba50f43f19600;hpb=bb7af347df386afcd3ea2adea8e7e982e3a5a253;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma b/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma
index 0b4c92e3e..5f00dc338 100644
--- a/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma
+++ b/helm/software/matita/contribs/dama/dama/models/nat_order_continuous.ma
@@ -12,12 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "models/nat_dedekind_sigma_complete.ma".
+include "models/increasing_supremum_stabilizes.ma".
 include "models/nat_ordered_uniform.ma".
 
 lemma nat_us_is_oc: ∀s:‡ℕ.order_continuity (segment_ordered_uniform_space ℕ s).
 intros 3; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H;
-[1: cases (nat_dedekind_sigma_complete s a H1 ? H2); 
+[1: cases (increasing_supremum_stabilizes s a H1 ? H2); 
     exists [apply w1]; intros; 
     apply (restrict nat_ordered_uniform_space s ??? H4);     
     generalize in match (H ? H5);
@@ -26,7 +26,7 @@ intros 3; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H;
     generalize in match (a i) in ⊢ (?? % ? → %); intro X; cases X; clear X;  
     intro; rewrite < H9 in H7; simplify; rewrite < H7; simplify;
     apply (us_phi1 nat_uniform_space ? H3); simplify; apply (eq_reflexive (us_carr nat_uniform_space));
-|2: cases (nat_dedekind_sigma_complete_r s a H1 ? H2); 
+|2: cases (increasing_supremum_stabilizes_r s a H1 ? H2); 
     exists [apply w1]; intros; 
     apply (restrict nat_ordered_uniform_space s ??? H4);     
     generalize in match (H ? H5);