proposition: Lemma increasing_is_increasing3 : forall (s : seq R), (increasing s) -> (forall k l, (k < (size s))%N -> (l < (size s))%N -> (k <= l)%N -> s`_k <= s`_l).
proof: Proof. case=> [ | a ] // => l. elim : l a => [a Hs k | b tl IHl a /andP Habtl k] [_ _ Hk | l] //. + rewrite leqn0 in Hk; by rewrite (eqP Hk). - rewrite leqn0 in Hk; by rewrite (eqP Hk). + case : k => [Hk Hl Hkl| k Hk Hl Hkl]. case : l Hl Hkl => [Hl Hkl |l Hl Hkl]. exact: (proj1 Habtl). apply: (@le_trans _ _ b). exact: (proj1 Habtl). apply: (IHl b (proj2 Habtl) 0%N l.+1) => //. by apply: (IHl b (proj2 Habtl)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)