proposition: Lemma mFT_cent_proper H : H :!=: 1 -> 'C(H) \proper G.
proof: Proof. case: (eqsVneq H G) => [-> | ]. by rewrite cent_mFT_trivial properT eq_sym. rewrite -properT => prH ntH; apply: sub_proper_trans (cent_sub H) _. exact: 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)