proposition: Theorem noncyclic_cent1_sub_Uniqueness p M B : M \in 'M -> B \in 'E_p(M) -> ~~ cyclic B -> \bigcup_(b in B^#) 'C[b] \subset M -> B \in 'U.
proof: Proof. move=> maxM EpB ncycB sCB_M. apply: (noncyclic_normed_sub_Uniqueness maxM EpB) => //. apply/bigcupsP=> K; rewrite inE -andbA => /and3P[_ p'K nKB]. case/pElemP: EpB => _ /and3P[pB cBB _]. rewrite -(coprime_abelian_gen_cent1 cBB ncycB nKB); last first. by rewrite coprime_sym (pnat_coprime pB). rewrite gen_subG (subset_trans _ sCB_M) //. by apply/bigcupsP=> b Bb; rewrite (bigcup_max b) // subsetIr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div fintype path) mathcomp(finset prime fingroup action automorphism quotient cyclic) mathcomp(gproduct gfunctor pgroup center commutator gseries nilpotent) mathcomp(sylow abelian maximal hall) odd_order(BGsection1 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection8)