proposition: Lemma zip_perm_tuple (B : finType) n (a : n.-tuple A) (b : n.-tuple B) (s : 'S_n) : zip_tuple (perm_tuple s a) (perm_tuple s b) = perm_tuple s (zip_tuple a b).
proof: Proof. apply eq_from_tnth; case. destruct n as [|n] => //. case=> [Hi | i Hi]. rewrite (tnth_nth (thead a, thead b)) (tnth_nth (thead (zip_tuple a b))). rewrite /= enum_ordSl /= (tnth_nth (thead a, thead b)) /= nth_zip; last first. by rewrite (size_tuple a) (size_tuple b). by rewrite (tnth_nth (thead a)) /= (tnth_nth (thead b)). rewrite (tnth_nth (thead a, thead b)) (tnth_nth (thead (zip_tuple a b))) /=. rewrite enum_ordSl /= nth_zip; last by rewrite 4!size_map size_enum_ord. rewrite [in RHS](nth_map ord0); last by rewrite size_map size_enum_ord. rewrite [in RHS](tnth_nth (thead a, thead b)) [in RHS]/zip_tuple /=. rewrite [in RHS]nth_zip; last by rewrite (size_tuple a) (size_tuple b). rewrite (nth_map ord0); last by rewrite size_map size_enum_ord. rewrite (nth_map ord0); last by rewrite size_map size_enum_ord. by rewrite (tnth_nth (thead a)) (tnth_nth (thead b)). Qed.
imports: mathcomp(all_ssreflect fingroup perm)