proposition: Lemma sub_nilpotent_cent2 H K G : nilpotent G -> K \subset G -> H \subset G -> coprime #|K| #|H| -> H \subset 'C(K).
proof: Proof. move=> nilG sKG sHG; rewrite coprime_pi' // => p'H. have sub_Gp := sub_Hall_pcore (nilpotent_pcore_Hall _ nilG). have [_ _ cGpp' _] := dprodP (nilpotent_pcoreC \pi(K) nilG). by apply: centSS cGpp'; rewrite sub_Gp ?pgroup_pi. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)