proposition: Lemma morphim_subcent1 A x : x \in D -> f @* 'C_A[x] \subset 'C_(f @* A)[f x].
proof: Proof. by move=> Dx; rewrite -(morphim_set1 Dx) morphim_subnorm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)