- ∀x.x is_supremum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
-intros 4; cases x (s Hs); clear x; letin X ≝ ≪s,Hs≫;
+ ∀X.X is_supremum a → ∃i.∀j.i ≤ j → \fst X = \fst (a j).
+intros 4; cases X (x Hx); clear X; letin X ≝ ≪x,Hx≫;
-letin spec ≝ (λi,j:ℕ.(𝕦_sg ≤ i ∧ s = \fst (a j)) ∨ (i < 𝕦_sg ∧ s + i ≤ 𝕦_sg + \fst (a j)));
-(* s - aj <= max 0 (u - i) *)
+letin spec ≝ (λi,j:ℕ.(𝕦_sg ≤ i ∧ x = \fst (a j)) ∨ (i < 𝕦_sg ∧ x + i ≤ 𝕦_sg + \fst (a j)));
+(* x - aj <= max 0 (u - i) *)
[ cmp_le _ ⇒ pred
| cmp_gt nP ⇒ \fst (H3 apred ?)]]
in aux
:
∀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;
[ cmp_le _ ⇒ pred
| cmp_gt nP ⇒ \fst (H3 apred ?)]]
in aux
:
∀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;
- generalize in match Hs;
- rewrite > (?:s = O);
- [2: cases Hs; lapply (os_le_to_nat_le ?? H1);
- apply (symmetric_eq nat O s ?).apply (le_n_O_to_eq s ?).apply (Hletin).
+ 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).
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);]
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 (le_to_or_lt_eq ?? H5); [2: assumption]
cases (?:False); apply (H2 (aux n1) H6);] clear H5;
generalize in match Hcut; clear Hcut; intro H5;
cases (le_to_or_lt_eq ?? H5); [2: assumption]
cases (?:False); apply (H2 (aux n1) H6);] clear H5;
generalize in match Hcut; clear Hcut; intro H5;
[1,3: left; split; [1,3: assumption |2: assumption]
cut (𝕦_sg = S n1); [2: apply le_to_le_to_eq; assumption ]
clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
[1,3: left; split; [1,3: assumption |2: assumption]
cut (𝕦_sg = S n1); [2: apply le_to_le_to_eq; assumption ]
clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
|*: right; split; try assumption;
[1: rewrite > sym_plus in ⊢ (? ? %);
rewrite < H6; apply le_plus_r; assumption;
|2: cases (H3 (a w) H6);
|*: right; split; try assumption;
[1: rewrite > sym_plus in ⊢ (? ? %);
rewrite < H6; apply le_plus_r; assumption;
|2: cases (H3 (a w) H6);
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;
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;
- ∀i,bound.∃j.i + bound = 𝕦_sg → s = \fst (a j));
-[1: cases (find (S n) n2); intro; change with (s = \fst (a w));
+ ∀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 (not_le_Sn_n ? H4)]
clearbody find; cases (find O 𝕦_sg);
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 (not_le_Sn_n ? H4)]
clearbody find; cases (find O 𝕦_sg);
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));
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));