proposition: Lemma cent_mFT_trivial : 'C(G) = 1.
proof: Proof. apply/eqP; apply: contraR mFT_nonAbelian => ntC. rewrite /abelian subTset /= eqEproper subsetT /=; apply/negP=> prC. have:= mFT_norm_proper ntC prC. by rewrite /proper subsetT norms_cent ?normG. 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)