proposition: Lemma zip_mask : forall bs l (k : seq B), zip (mask bs l) (mask bs k) = mask bs (zip l k).
proof: Proof. elim=> // h t IH [|a1 a2] [|b1 b2] //=. - destruct h => //=; by case: mask. - destruct h => //=; by case: mask. - destruct h => /=; by rewrite IH. Qed.
imports: mathcomp(all_ssreflect fingroup perm)