proposition: Lemma morphpre_cent1s R x : x \in D -> R \subset f @* D -> f @*^-1 R \subset 'C[x] -> R \subset 'C[f x].
proof: Proof. by move=> Dx sRfD; move/(morphim_cent1s Dx); rewrite morphpreK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)