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