+
+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;
+
+