proposition: Lemma seqmul_coef (s1 s2 : seq R) k : (k < minn (size s1) (size s2))%N -> (seqmul s1 s2)`_k = s1`_k * s2`_k.
proof: Proof. move=> Hk. rewrite (nth_map 0); last by rewrite size_zip. by rewrite nth_zip_cond size_zip Hk /=. 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)