proposition: Lemma meet_center_nil G H : nilpotent G -> H <| G -> H :!=: 1 -> H :&: 'Z(G) != 1.
proof: Proof. by move=> nilG nsHG; apply: contraNneq => /TI_center_nil->. 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)