proposition: Lemma center_ncprod n : 'Z(G_ n) \isog 'Z(G).
proof: Proof. elim: n => [|n]; first by rewrite center_ncprod0 ncprod0. rewrite [ncprod]unlock=> /isog_symr/xcprodP[gz isoZ] /=. by rewrite -cpairg1_center isog_sym sub_isog ?center_sub ?injm_cpairg1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(cyclic)