proposition: Lemma morphpre_cent A : 'C_D(A) \subset f @*^-1 'C(f @* A).
proof: Proof. rewrite -sub_morphim_pre ?subsetIl // morphimGI ?(subsetIl, subIset) // orbC. by rewrite (subset_trans (morphim_cent _)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)