proposition: Lemma perm_tuple_inj n (s : 'S_n) : injective (@perm_tuple A n s).
proof: Proof. move=> a b H. have : perm_tuple 1 a = perm_tuple 1 b by rewrite -(mulVg s) -!perm_tuple_comp H. rewrite !perm_tuple_id; apply. Qed.
imports: mathcomp(all_ssreflect fingroup perm)