1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "dama/models/increasing_supremum_stabilizes.ma".
16 include "dama/models/nat_ordered_uniform.ma".
18 lemma nat_us_is_oc: ∀s:‡ℕ.order_continuity (segment_ordered_uniform_space ℕ s).
19 intros 3; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H;
20 [1: cases (increasing_supremum_stabilizes s a H1 ? H2);
21 exists [apply w1]; intros;
22 apply (restrict nat_ordered_uniform_space s ??? H4);
23 generalize in match (H ? H5);
25 generalize in match (refl_eq ? (a i):a i = a i);
26 generalize in match (a i) in ⊢ (?? % ? → %); intro X; cases X; clear X;
27 intro; rewrite < H9 in H7; simplify; rewrite < H7; simplify;
28 apply (us_phi1 nat_uniform_space ? H3); simplify; apply (eq_reflexive (us_carr nat_uniform_space));
29 |2: cases (increasing_supremum_stabilizes_r s a H1 ? H2);
30 exists [apply w1]; intros;
31 apply (restrict nat_ordered_uniform_space s ??? H4);
32 generalize in match (H ? H5);
34 generalize in match (refl_eq ? (a i):a i = a i);
35 generalize in match (a i) in ⊢ (?? % ? → %); intro X; cases X; clear X;
36 intro; rewrite < H9 in H7; simplify; rewrite < H7; simplify;
37 apply (us_phi1 nat_uniform_space ? H3); simplify; apply (eq_reflexive (us_carr nat_uniform_space));]