fact: Definition seqmul := (fun s1 s2 : seq R => map (fun x : R * R => x.1 * x.2) (zip s1 s2)).
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)