proposition: Lemma injm_cent A : A \subset D -> f @* 'C(A) = 'C_(f @* D)(f @* A).
proof: Proof. move=> sAD; apply/eqP; rewrite -morphimIdom eqEsubset morphim_subcent. apply/subsetP=> fx; case/setIP; case/morphimP=> x Dx _ ->{fx} cAfx. rewrite mem_morphim // inE Dx -sub1set centsC cent_set1 -injmSK //. by rewrite injm_cent1 // subsetI morphimS // -cent_set1 centsC sub1set. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)