proposition: Lemma nil_class0 G : (nil_class G == 0) = (G :==: 1).
proof: Proof. apply/idP/eqP=> [nilG | ->]. by apply/(lcn_nil_classP 0); rewrite ?nilpotent_class (eqP nilG) ?cardG_gt0. by rewrite -leqn0; apply/(lcn_nil_classP 0); rewrite ?nilpotent1. 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)