proposition: Lemma TI_center_nil G H : nilpotent G -> H <| G -> H :&: 'Z(G) = 1 -> H :=: 1.
proof: Proof. move=> nilG /andP[sHG nHG] tiHZ. rewrite -{1}(setIidPl sHG); have{nilG} /ucnP[n <-] := nilG. elim: n => [|n IHn]; apply/trivgP; rewrite ?subsetIr // -tiHZ. rewrite [H :&: 'Z(G)]setIA subsetI setIS ?ucn_sub //= (sameP commG1P trivgP). rewrite -commg_subr commGC in nHG. rewrite -IHn subsetI (subset_trans _ nHG) ?commSg ?subsetIl //=. by rewrite (subset_trans _ (ucn_comm n G)) ?commSg ?subsetIr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype div bigop prime finset fingroup morphism) mathcomp(automorphism quotient commutator gproduct) mathcomp(gfunctor center gseries cyclic)