proposition: Lemma card_Alt : 1 < n -> (2 * #|'Alt_T|)%N = n`!.
proof: Proof. by move/Alt_index <-; rewrite mulnC (Lagrange Alt_subset) card_Sym. 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)