proposition: Lemma simple_Alt_3 (T : finType) : #|T| = 3 -> simple 'Alt_T.
proof: Proof. move=> T3; have{T3} oA: #|'Alt_T| = 3. by apply: double_inj; rewrite -mul2n card_Alt T3. apply/simpleP; split=> [|K]; [by rewrite trivg_card1 oA | case/andP=> sKH _]. have:= cardSg sKH; rewrite oA dvdn_divisors // !inE orbC /= -oA. case/pred2P=> eqK; [right | left]; apply/eqP. by rewrite eqEcard sKH eqK leqnn. by rewrite eq_sym eqEcard sub1G eqK cards1. 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)