lapply (H6 H4) as H7; apply eq_sym; apply H7;]]
qed.
+
+notation "\naturals" non associative with precedence 99 for @{'nat}.
+
+interpretation "naturals" 'nat = nat.
+interpretation "Ordered set N" 'nat = nat_ordered_set.
+
+lemma nat_dedekind_sigma_complete:
+ ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing →
+ ∀x.x is_supremum a → ∃i.∀j.i ≤ j → x ≈ a j.
+intros 5; cases x; clear x; intros;
+cases H2;
+letin m ≝ (
+ let rec aux i ≝
+ match i with
+ [ O ⇒ match eqb (fst (a O)) x1 with
+ [ true ⇒ O
+ | false ⇒ match H4 (a O) ? with
+ [ ex_introT n _ ⇒ n]]
+ | S m ⇒ let pred ≝ aux m in
+ match eqb (fst (a pred)) x1 with
+ [ true ⇒ pred
+ | false ⇒ match H4 (a pred) ? with
+ [ ex_introT n _ ⇒ n]]]
+ in aux
+ :
+ ∀i:nat.∃j.a j = x1 ∨ a i < a j);
+
+cases (∀n.a n = x1 ∨ x1 ≰ a n);
+
+ elim x1 in H1 ⊢ % 0;
+[1: intro H2; letin X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) O H2); intros;
+ fold unfold X X in H1 ⊢ %;
+ exists [apply O] cases H1; intros; apply le_le_eq;[2: apply H3;]
+ intro; alias symbol "pi1" = "sigma pi1".
+ change in H6 with (fst (a j) < O);
+ apply (not_le_Sn_O (fst (a j))); apply H6;
+|2: intros 3; letin S_X ≝ (sig_in ℕ (λx:ℕ.x∈[l,u]) (S n) H2); intros;
+ fold unfold S_X S_X in H3 ⊢ %;
+ generalize in match (leb_to_Prop l n); elim (leb l n); simplify in H4;
+ [1: cut (n ≤ u); [2: cases H2; normalize in H5 ⊢ %;
+ apply le_S_S_to_le; lapply (not_lt_to_le ?? H5) as XX;
+ apply le_S; apply XX;]
+ cases H1; [2:split; apply nat_le_to_os_le; assumption|3:simplify;
+
+ elim (or_lt_le (S n) l);
+ [ cases (?:l = S n ∨ l < S n);[
+ unfold lt; cases H2; normalize in H5;
+ apply (Right (eq nat n (S n)) (lt n (S n)) ?).apply (not_le_to_lt (S n) n ?).apply (not_le_Sn_n n).]
+ [ destruct H4;
+
+
+ ∀x.∃i.x ≰ a i ∨ x ≤ a i.
+intros; elim x;
+
+
definition nat_uniform_space: uniform_space.
-apply (discrete_uniform_space_of_bishop_set nat_ordered_set);
+apply (discrete_uniform_space_of_bishop_set ℕ);
qed.
+
+interpretation "Uniform space N" 'nat = nat_uniform_space.
+
+include "ordered_uniform.ma".
+
+definition nat_ordered_uniform_space:ordered_uniform_space.
+apply (mk_ordered_uniform_space (mk_ordered_uniform_space_ ℕ ℕ (refl_eq ? ℕ)));
+simplify; intros 7; cases H3; cases H4; cases H5; clear H5 H4;
+cases H (_); cases (H4 y); apply H5; clear H5 H10; cases (H4 p);
+lapply (H10 H1) as H11; clear H10 H5; apply (le_le_eq);
+[1: apply (le_transitive ???? H6); apply (Le≪ ? H11); assumption;
+|2: apply (le_transitive ????? H7); apply (Le≫ (snd p) H11); assumption;]
+qed.
+
+interpretation "Uniform space N" 'nat = nat_ordered_uniform_space.
+
+lemma nat_us_is_oc: ∀l,u:ℕ.order_continuity {[l,u]}.
+intros 4; split; intros 3; cases H; cases H3; clear H3 H;
+cases (H5 (a i));
+cases (H10 (sig_in ?? x1 H2));
+
+exists [1,3:apply x1]
+intros; apply H6;
include "ordered_set.ma".
include "nat/compare.ma".
-include "cprop_connectives.ma".
+include "cprop_connectives.ma".
definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
[1: intro x; intro; apply (not_le_Sn_n ? H);
|2: apply nat_excess_cotransitive]
qed.
+
+alias id "le" = "cic:/matita/dama/ordered_set/le.con".
+lemma os_le_to_nat_le:
+ ∀a,b:nat_ordered_set.le nat_ordered_set a b → a ≤ b.
+intros; normalize in H; apply (not_lt_to_le ?? H);
+qed.
+
+lemma nat_le_to_os_le:
+ ∀a,b:nat_ordered_set.a ≤ b → le nat_ordered_set a b.
+intros 3; apply (le_to_not_lt a b);assumption;
+qed.
+
\ No newline at end of file