-letin m ≝ (? : sequence nat_ordered_set); [
- apply (hide (nat→nat)); intro i; elim i (i' Rec);
- [1: apply (hide nat);cases (H2 ? (H8 0)) (k _); apply k;
- |2: apply (max (hide nat ?) (S Rec)); cases (H2 ? (H8 (S i'))) (k Hk);apply k]]
-cut (m is_strictly_increasing) as Hm; [2:
- intro n; change with (S (m n) ≤ m (S n)); unfold m; whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]
-lapply (selection ?? Hm a l H1) as H10;
-lapply (H9 ?? H10) as H11;
-[1: exists [apply (m 0)] intros;
- apply (ous_convex ?? H3 ? H11 (H6 (m 0)));
- simplify; repeat split;
-
-
-
\ No newline at end of file
+letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
+ match i with
+ [ O ⇒ match H2 (w i) ? with [ ex_introT k _ ⇒ k ]
+ | S i' ⇒ max (match H2 (w i) ? with [ ex_introT k _ ⇒ k ]) (S (aux i'))
+ ] in aux
+ :
+ ∀z:nat.∃k:nat.∀i,j,l.k ≤ i → k ≤ j → l ≤ z → w l 〈a i, a j〉));
+ [1,2:apply H8;
+ |3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?);
+ simplify in ⊢ (?→? (? % ?) ?→?);
+ intros; lapply (H10 i j) as H14;
+ [2: apply (max_le_l ??? H11);|3:apply (max_le_l ??? H12);]
+ cases (le_to_or_lt_eq ?? H13); [2: destruct H15; destruct H5; assumption]
+ generalize in match H11; generalize in match H12;
+ cases (aux n1); simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
+ apply H16; [3: apply le_S_S_to_le; assumption]
+ apply lt_to_le; apply (max_le_r w1); assumption;
+ |4: intros; clear H11; rewrite > H5 in H10;
+ rewrite < (le_n_O_to_eq ? H14); apply H10; assumption;]
+cut (((m : nat→nat) : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2:
+ intro n; change with (S (m n) ≤ m (S n)); unfold m;
+ whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]
+cut (((m : nat→nat) : sequence nat_ordered_set) is_increasing) as Hm1; [2:
+ intro n; intro L; change in L with (m (S n) < m n);
+ lapply (Hm n) as L1; change in L1 with (m n < m (S n));
+ lapply (trans_lt ??? L L1) as L3; apply (not_le_Sn_n ? L3);]
+clearbody m;
+lapply (selection ?? Hm a l H1) as H10;
+lapply (H9 ?? H10) as H11; [
+ exists [apply (m 0:nat)] intros;
+ apply (ous_convex ?? H3 ? H11 (H6 (m 0)));
+ simplify; repeat split; [intro X; cases (os_coreflexive ?? X)|2,3:apply H6;]
+ change with (a (m O) ≤ a i);
+ apply (trans_increasing ?? H4); intro; whd in H12;
+ apply (not_le_Sn_n i); apply (transitive_le ??? H12 H5)]
+clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
+generalize in match (refl_eq nat (m q));
+generalize in match (m q) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
+intros; simplify in H12:(? ? ? %); simplify in ⊢ (? ? (? ? ? % ?));
+generalize in match (refl_eq nat (m r));
+generalize in match (m r) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
+intros; simplify in H14:(? ? ? %); simplify in ⊢ (? ? (? ? ? ? %));
+generalize in match (refl_eq nat (m p));
+generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
+intros; simplify in H16:(? ? ? %);
+apply H15; [3: apply le_n] destruct H16; destruct H14; destruct H12; clear H11 H13 H15;
+[1: lapply (trans_increasing ?? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
+ apply (le_to_not_lt p q H5);
+|2: lapply (trans_increasing ?? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
+ apply (le_to_not_lt p r H10);]
+qed.
\ No newline at end of file