(* *)
(**************************************************************************)
-include "models/nat_dedekind_sigma_complete.ma".
+include "models/increasing_supremum_stabilizes.ma".
include "models/nat_ordered_uniform.ma".
-lemma nat_us_is_oc: ∀l,u:ℕ.order_continuity (segment_ordered_uniform_space ℕ l u).
-intros 4; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H;
-[1: cases (nat_dedekind_sigma_complete l u a H1 ? H2);
+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 (increasing_supremum_stabilizes s a H1 ? H2);
exists [apply w1]; intros;
- apply (restrict nat_ordered_uniform_space l u ??? H4);
+ apply (restrict nat_ordered_uniform_space s ??? H4);
generalize in match (H ? H5);
cases x; intro;
generalize in match (refl_eq ? (a i):a i = a i);
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;
-|2: cases (nat_dedekind_sigma_complete_r l u a H1 ? H2);
+ apply (us_phi1 nat_uniform_space ? H3); simplify; apply (eq_reflexive (us_carr nat_uniform_space));
+|2: cases (increasing_supremum_stabilizes_r s a H1 ? H2);
exists [apply w1]; intros;
- apply (restrict nat_ordered_uniform_space l u ??? H4);
+ apply (restrict nat_ordered_uniform_space s ??? H4);
generalize in match (H ? H5);
cases x; intro;
generalize in match (refl_eq ? (a i):a i = a i);
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;]
+ apply (us_phi1 nat_uniform_space ? H3); simplify; apply (eq_reflexive (us_carr nat_uniform_space));]
qed.