proposition: Theorem Burnside_p_a_q_b gT (G : {group gT}) : (size (primes #|G|) <= 2)%N -> solvable G.
proof: Proof. move: {2}_.+1 (ltnSn #|G|) => n; elim: n => // n IHn in gT G *. rewrite ltnS => leGn piGle2; have [simpleG | ] := boolP (simple G); last first. rewrite negb_forall_in => /exists_inP[N sNG]; rewrite eq_sym. have [->|] := eqVneq N G. rewrite groupP /= genGid normG andbT eqb_id negbK => /eqP->. exact: solvable1. rewrite [N == G]eqEproper sNG eqbF_neg !negbK => ltNG /and3P[grN]. case/isgroupP: grN => {}N -> in sNG ltNG *; rewrite /= genGid => ntN nNG. have nsNG: N <| G by apply/andP. have dv_le_pi m: (m %| #|G| -> size (primes m) <= 2)%N. move=> m_dv_G; apply: leq_trans piGle2. by rewrite uniq_leq_size ?primes_uniq //; apply: pi_of_dvd. rewrite (series_sol nsNG) !IHn ?dv_le_pi ?cardSg ?dvdn_quotient //. by apply: leq_trans leGn; apply: ltn_quotient. by apply: leq_trans leGn; apply: proper_card. have [->|[p p_pr p_dv_G]] := trivgVpdiv G; first exact: solvable1. have piGp: p \in \pi(G) by rewrite mem_primes p_pr cardG_gt0. have [P sylP] := Sylow_exists p G; have [sPG pP p'GP] := and3P sylP. have ntP: P :!=: 1%g by rewrite -rank_gt0 (rank_Sylow sylP) p_rank_gt0. have /trivgPn[g /setIP[Pg cPg] nt_g]: 'Z(P) != 1%g. by rewrite center_nil_eq1 // (pgroup_nil pP). apply: abelian_sol; have: (size (primes #|g ^: G|) <= 1)%N. rewrite -ltnS -[_.+1]/(size (p :: _)) (leq_trans _ piGle2) //. rewrite -index_cent1 uniq_leq_size // => [/= | q]. rewrite primes_uniq -p'natEpi ?(pnat_dvd _ p'GP) ?indexgS //. by rewrite subsetI sPG sub_cent1. by rewrite inE => /predU1P[-> // |]; apply: pi_of_dvd; rewrite ?dvdn_indexg. rewrite leqNgt; apply: contraR => /primes_class_simple_gt1-> //. by rewrite !inE classG_eq1 nt_g mem_classes // (subsetP sPG). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient action countalg finalg zmodp) mathcomp(commutator cyclic center pgroup sylow gseries) mathcomp(nilpotent abelian ssrnum ssrint archimedean polydiv) mathcomp(rat matrix mxalgebra intdiv mxpoly vector falgebra) mathcomp(fieldext separable galois algC cyclotomic algnum) mathcomp(mxrepresentation classfun character)