proposition: Lemma minSimpleOdd_ind gT (G : {group gT}) : odd #|G| -> solvable G.
proof: Proof. move: {2}_.+1 (ltnSn #|G|) => n. elim: n => // n IHn in gT G *; rewrite ltnS => leGn oddG. have oG: #|[subg G]| = #|G| by rewrite (card_isog (isog_subg G)). apply/idPn=> nsolG; apply: IH_FT. pose gT' : finGroupType := subg_of G. apply: (HB.pack gT' (IsMinSimpleOddGroup.Build gT' _ _ _ _)); do ?[move=> /= ??????]. - by rewrite oG. - rewrite -(isog_simple (isog_subg _)); apply/simpleP; split=> [|H nsHG]. by apply: contra nsolG; move/eqP->; rewrite abelian_sol ?abelian1. have [sHG _]:= andP nsHG; apply/pred2P; apply: contraR nsolG; case/norP=> ntH. rewrite eqEcard sHG -ltnNge (series_sol nsHG) => ltHG. by rewrite !IHn ?(oddSg sHG) ?quotient_odd ?(leq_trans _ leGn) ?ltn_quotient. - by apply: contra nsolG => solG; rewrite -(im_sgval G) morphim_sol. move=> M; rewrite properEcard oG; case/andP=> sMG ltMG. by apply: IHn (leq_trans ltMG leGn) (oddSg sMG _); rewrite oG. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div choice fintype bigop) mathcomp(finset prime fingroup morphism automorphism action quotient) mathcomp(gfunctor cyclic pgroup center commutator gseries nilpotent) mathcomp(sylow abelian maximal hall) odd_order(BGsection1 BGsection6)