proposition: Lemma morphim_subcent A B : f @* 'C_A(B) \subset 'C_(f @* A)(f @* B).
proof: Proof. exact: subset_trans (morphimI A _) (setIS _ (morphim_cent B)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)