proposition: Lemma mask_zip : forall (b : bitseq) (s1 s2 : seq R), mask b (zip s1 s2) = zip (mask b s1) (mask b s2).
proof: Proof. elim => [ | a l IHl] //. case => [s2 |x s1 ] //. by rewrite /= !zip_nil_1. case=> [ |y s2 /=] //. by rewrite zip_nil_2 !mask0 zip_nil_2. case Ha : a => //. by rewrite IHl. 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)