proposition: Lemma card_Sym : #|'Sym_T| = n`!.
proof: Proof. rewrite -[n]cardsE -card_perm; apply: eq_card => p. by apply/idP/subsetP=> [? ?|]; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype tuple tuple bigop prime finset fingroup) mathcomp(morphism perm automorphism quotient action cyclic) mathcomp(pgroup gseries sylow primitive_action)