proposition: Lemma Aut_cprod_by_full : Aut_in (Aut H) 'Z(H) \isog Aut 'Z(H) -> Aut_in (Aut K) 'Z(K) \isog Aut 'Z(K) -> Aut_in (Aut C) 'Z(C) \isog Aut 'Z(C).
proof: Proof. move=> AutZinH AutZinK. have Cfull:= Aut_cprod_full im_cpair_cprod cpair_center_id. by rewrite Cfull // -injm_center // injm_Aut_full ?center_sub. 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)