proposition: Lemma Aut_ncprod_full n : Aut_in (Aut G) 'Z(G) \isog Aut 'Z(G) -> Aut_in (Aut (G_ n)) 'Z(G_ n) \isog Aut 'Z(G_ n).
proof: Proof. move=> AutZinG; elim: n => [|n IHn]. by rewrite center_ncprod0; apply/Aut_sub_fullP=> // g injg gG0; exists g. by case: ncprodS => gz isoZ; apply: Aut_cprod_by_full. 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)