proposition: Lemma filter_zip_R m (l : seq A) (k : seq B) b : size l = m -> size k = m -> filter (fun x => x.2 == b) (zip l k) = zip (mask (map (pred1 b) k) l) (filter (pred1 b) k).
proof: Proof. move=> Hl Hk. rewrite filter_mask [in RHS]filter_mask zip_mask; congr mask. elim: m l k Hl Hk b => [[] // [] // | n ih]. move=> [|a1 a2] // [|b1 b2] // [sza2] [szb2] b /=; by rewrite ih. Qed.
imports: mathcomp(all_ssreflect fingroup perm)