proposition: Lemma trivial_Alt_2 (T : finType) : #|T| <= 2 -> 'Alt_T = 1.
proof: Proof. rewrite leq_eqVlt => /predU1P[] oT. by apply: card_le1_trivg; rewrite -leq_double -mul2n card_Alt oT. suffices Sym1: 'Sym_T = 1 by apply/trivgP; rewrite -Sym1 subsetT. by apply: card1_trivg; rewrite card_Sym; case: #|T| oT; do 2?case. 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)