proposition: Lemma ucnE n A : 'Z_n(A) = iter n (fun B => coset B @*^-1 'Z(A / B)) 1.
proof: Proof. by []. 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)