proposition: Lemma subseq_incr (s1 s2 : seq R) : subseq s1 s2 -> increasing s2 -> increasing s1.
proof: Proof. rewrite /increasing. apply: subseq_sorted => //. exact: le_trans. 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)