alias symbol "pi1" = "exT \fst".
alias symbol "N" = "ordered set N".
+alias symbol "dependent_pair" = "dependent pair".
lemma increasing_supremum_stabilizes:
∀sg:‡ℕ.∀a:sequence {[sg]}.
a is_increasing →
intros 4; cases X (x Hx); clear X; letin X ≝ ≪x,Hx≫;
fold normalize X; intros; cases H1;
alias symbol "N" = "Natural numbers".
-letin spec ≝ (λi,j:ℕ.(𝕦_sg ≤ i ∧ x = \fst (a j)) ∨ (i < 𝕦_sg ∧ x + i ≤ 𝕦_sg + \fst (a j)));
+letin spec ≝ (λi,j:ℕ.(𝕦_ sg ≤ i ∧ x = \fst (a j)) ∨ (i < 𝕦_ sg ∧ x + i ≤ 𝕦_ sg + \fst (a j)));
(* x - aj <= max 0 (u - i) *)
letin m ≝ (hide ? (
let rec aux i ≝
∀i:nat.∃j:nat.spec i j));[whd; apply nP;] unfold spec in aux ⊢ %;
[3: unfold X in H2; clear H4 n aux spec H3 H1 H X;
cases (cases_in_segment ??? Hx);
- elim 𝕦_sg in H1 ⊢ %; intros (a Hs H);
+ elim 𝕦_ sg in H1 ⊢ %; intros (a Hs H);
[1: left; split; [apply le_n]
generalize in match H;
generalize in match Hx;
rewrite > (?:x = O);
[2: cases Hx; lapply (os_le_to_nat_le ?? H1);
apply (symmetric_eq nat O x ?).apply (le_n_O_to_eq x ?).apply (Hletin).
- |1: intros; unfold Type_of_ordered_set in sg;
+ |1: intros; unfold Type_OF_ordered_set in sg a; whd in a:(? %);
lapply (H2 O) as K; lapply (sl2l_ ?? (a O) ≪x,Hx≫ K) as P;
simplify in P:(???%); lapply (le_transitive ??? P H1) as W;
lapply (os_le_to_nat_le ?? W) as R; apply (le_n_O_to_eq (\fst (a O)) R);]
cases H5; clear H5; cases H7; clear H7;
[1: left; split; [ apply (le_S ?? H5); | assumption]
|3: cases (?:False); rewrite < H8 in H6; apply (not_le_Sn_n ? H6);
- |*: cases (cmp_nat 𝕦_sg (S n1));
+ |*: cases (cmp_nat 𝕦_ sg (S n1));
[1,3: left; split; [1,3: assumption |2: assumption]
- cut (𝕦_sg = S n1); [2: apply le_to_le_to_eq; assumption ]
+ cut (𝕦_ sg = S n1); [2: apply le_to_le_to_eq; assumption ]
clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
cut (x = S (\fst (a w)));
[2: apply le_to_le_to_eq; [2: assumption]
[1: rewrite > sym_plus in ⊢ (? ? %);
rewrite < H6; apply le_plus_r; assumption;
|2: cases (H3 (a w) H6);
- change with (x + S n1 ≤ 𝕦_sg + \fst (a w1));rewrite < plus_n_Sm;
+ change with (x + S n1 ≤ 𝕦_ sg + \fst (a w1));rewrite < plus_n_Sm;
apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm;
apply (le_plus ???? (le_n ?) H9);]]]]
clearbody m; unfold spec in m; clear spec;
+alias symbol "exists" = "CProp exists".
letin find ≝ (
let rec find i u on u : nat ≝
match u with
| false ⇒ find (S i) w]]
in find
:
- ∀i,bound.∃j.i + bound = 𝕦_sg → x = \fst (a j));
+ ∀i,bound.∃j.i + bound = 𝕦_ sg → x = \fst (a j));
[1: cases (find (S n) n2); intro; change with (x = \fst (a w));
apply H6; rewrite < H7; simplify; apply plus_n_Sm;
|2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity
|3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1;
- cases (m 𝕦_sg); cases H4; clear H4; cases H5; clear H5; [assumption]
+ cases (m 𝕦_ sg); cases H4; clear H4; cases H5; clear H5; [assumption]
cases (not_le_Sn_n ? H4)]
-clearbody find; cases (find O 𝕦_sg);
+clearbody find; cases (find O 𝕦_ sg);
exists [apply w]; intros; change with (x = \fst (a j));
rewrite > (H4 ?); [2: reflexivity]
apply le_to_le_to_eq;
[1: apply os_le_to_nat_le;
- apply (trans_increasing ? H ? ? (nat_le_to_os_le ?? H5));
+ apply (trans_increasing a H ? ? (nat_le_to_os_le ?? H5));
|2: apply (trans_le ? x ?);[apply os_le_to_nat_le; apply (H2 j);]
rewrite < (H4 ?); [2: reflexivity] apply le_n;]
qed.