proposition: Lemma mask_seqmul (b : bitseq) (s1 s2 : seq R) : mask b (seqmul s1 s2) = seqmul (mask b s1) (mask b s2).
proof: Proof. by rewrite -map_mask mask_zip. 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)