proposition: Lemma increasingP (s : seq R) : reflect (forall k, (k < (size s).-1)%N -> s`_k <= s`_k.+1) (increasing s).
proof: Proof. apply/(iffP idP) => [H k Hk | H]. case: s H k Hk => [ | a ] // => l. elim : l a => [ | b tl IHl a /andP Habtl] //. case => [_ | n Hn] //=. exact: (proj1 Habtl). apply: (IHl b (proj2 Habtl)). by rewrite -(ltn_add2r 1%N) !addn1 prednK. case: s H => [ | a] => // => l. elim : l a => [ | b l IHs a Hk] //. apply/andP; split. apply: (Hk 0%N) => //. apply: (IHs b) => k Hkk. by rewrite (Hk k.+1) // -(addn1 k) addnC -ltn_subRL subn1. 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)