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 "models/nat_uniform.ma".
16 include "bishop_set_rewrite.ma".
17 include "ordered_uniform.ma".
19 definition nat_ordered_uniform_space:ordered_uniform_space.
20 apply (mk_ordered_uniform_space (mk_ordered_uniform_space_ ℕ ℕ (refl_eq ? ℕ)));
21 simplify; intros 7; cases H3;
22 cases H (_); cases (H8 y); apply H9; cases (H8 p);
23 lapply (H12 H1) as H13; apply (le_le_eq);
24 [1: apply (le_transitive ???? H4); apply (Le≪ ? H13); assumption;
25 |2: apply (le_transitive ????? H5); apply (Le≫ (\snd p) H13); assumption;]
28 interpretation "Ordered uniform space N" 'N = nat_ordered_uniform_space.