proposition: Lemma morphim_cent A : f @* 'C(A) \subset 'C(f @* A).
proof: Proof. apply/bigcapsP=> fx; case/morphimP=> x Dx Ax ->{fx}. by apply: subset_trans (morphim_cent1 Dx); apply: morphimS; apply: bigcap_inf. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)