X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Fmodels%2Fnat_order_continuous.ma;h=3901c8b76b82413971adffeb1f9ca78a15da6835;hb=HEAD;hp=5f00dc338d217a855296d51c18985d6f7174467e;hpb=6fbeff97e37927fd95b3aee3eb23b4309fc465c4;p=helm.git diff --git a/helm/software/matita/library/dama/models/nat_order_continuous.ma b/helm/software/matita/library/dama/models/nat_order_continuous.ma index 5f00dc338..3901c8b76 100644 --- a/helm/software/matita/library/dama/models/nat_order_continuous.ma +++ b/helm/software/matita/library/dama/models/nat_order_continuous.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "models/increasing_supremum_stabilizes.ma". -include "models/nat_ordered_uniform.ma". +include "dama/models/increasing_supremum_stabilizes.ma". +include "dama/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;