proposition: Lemma tnth_zip_1 (B : finType) n (x1 : n.-tuple A) (x2 : n.-tuple B) i: (tnth [tuple of zip x1 x2] i).1 = tnth x1 i.
proof: Proof. rewrite /tnth; set def := tnth_default _ _; case: def => ? ?. rewrite nth_zip /=; last by rewrite !size_tuple. apply set_nth_default; by rewrite size_tuple. Qed.
imports: mathcomp(all_ssreflect fingroup perm)