proposition: Lemma quotient_ucn_add m n G : 'Z_(m + n)(G) / 'Z_n(G) = 'Z_m(G / 'Z_n(G)).
proof: Proof. elim: m => [|m IHm]; first exact: trivg_quotient. apply/setP=> Zx; have [x Nx ->{Zx}] := cosetP Zx. have [sZG nZG] := andP (ucn_normal n G). rewrite (ucnSnR m) inE -!sub1set -morphim_set1 //= -quotientR ?sub1set // -IHm. rewrite !quotientSGK ?(ucn_sub_geq, leq_addl, comm_subG _ nZG, sub1set) //=. by rewrite addSn /= ucnSnR inE. 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)