proposition: Lemma quotient_nil G H : nilpotent G -> nilpotent (G / H).
proof: Proof. exact: morphim_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)