proposition: Lemma subspseq_increasing : increasing (seqn0 spseq).
proof: Proof. by rewrite (@subseq_incr R _ spseq) // ?filter_subseq // ?spseq_increasing. 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)