proposition: Lemma mFT_quo_sol M H : H :!=: 1 -> solvable (M / H).
proof: Proof. move=> ntH; case: (eqsVneq H G) => [-> |]. rewrite [_ / _](trivgP _) ?abelian_sol ?abelian1 //. by rewrite quotient_sub1 ?normsG ?subsetT. rewrite -properT => prH; rewrite -quotientInorm morphim_sol //. by apply: solvableS (subsetIr _ _) (mFT_sol _); rewrite mFT_norm_proper. 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)