proposition: Lemma ext_norm_conj_cent (H : {group gT}) x : H \subset G -> x \in 'C_(G | to)(A) -> [acts A, on H :^ x | to] = [acts A, on H | to].
proof: Proof. move=> sHG /setIP[Gx]. rewrite gacentEsd !actsEsd ?conj_subG ?morphimJ // 2!inE Gx /=. exact: norm_conj_cent. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div choice) mathcomp(fintype finset prime fingroup morphism) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(commutator center pgroup finmodule nilpotent) mathcomp(sylow abelian maximal)