proposition: Lemma Alt_index : 1 < n -> #|'Sym_T : 'Alt_T| = 2.
proof: Proof. move=> lt1n; rewrite -card_quotient ?Alt_norm //=. have : ('Sym_T / 'Alt_T) \isog (@odd_perm T @* 'Sym_T) by apply: first_isog. case/isogP=> g /injmP/card_in_imset <-. rewrite /morphim setIid=> ->; rewrite -card_bool; apply: eq_card => b. apply/imsetP; case: b => /=; last first. by exists (1 : {perm T}); [rewrite setIid inE | rewrite odd_perm1]. case: (pickP T) lt1n => [x1 _ | d0]; last by rewrite /n eq_card0. rewrite /n (cardD1 x1) ltnS lt0n => /existsP[x2 /=]. by rewrite eq_sym andbT -odd_tperm; exists (tperm x1 x2); 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)