proposition: Lemma seqmul_cons (s1 s2 : seq R) (a b : R) : seqmul (a::s1) (b::s2) = (a * b) :: (seqmul s1 s2).
proof: Proof. by rewrite /seqmul. 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)