proposition: Lemma mFT_norm_proper H : H :!=: 1 -> H \proper G -> 'N(H) \proper G.
proof: Proof. move=> ntH; rewrite !properT; apply: contra; move/eqP=> nHG; apply/eqP. move/eqP: ntH; case/simpleP : (@mFT_simple gT) => _; case/(_ H) => //=. by rewrite -nHG normalG. 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)