proposition: Lemma mFT_sol_proper M : (M \proper G) = solvable M.
proof: Proof. apply/idP/idP; first exact: mFT_sol. by rewrite properT; apply: contraL; move/eqP->; apply: mFT_nonSolvable. 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)