proposition: Lemma Alt_even p : (p \in 'Alt_T) = ~~ p.
proof: Proof. by rewrite !inE /=; case: odd_perm. 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)