proposition: Lemma morphpre_cent1 x : x \in D -> 'C_D[x] \subset f @*^-1 'C[f x].
proof: Proof. move=> Dx; rewrite -sub_morphim_pre ?subsetIl //. by apply: subset_trans (morphim_cent1 Dx); rewrite morphimS ?subsetIr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)