proposition: Lemma spseq_size : size spseq = d.-2.
proof: Proof. by rewrite /spseq size_map size_zip size_drop subn1 -p_size minnE subKn // leq_pred. 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)