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