proposition: Lemma morphim_cents A B : A \subset 'C(B) -> f @* A \subset 'C(f @* B).
proof: Proof. by move=> cBA; apply: subset_trans (morphim_cent B); apply: morphimS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)