proposition: Lemma injm_cents A B : A \subset D -> B \subset D -> (f @* A \subset 'C(f @* B)) = (A \subset 'C(B)).
proof: Proof. by move=> sAD sBD; rewrite -injmSK // injm_cent // subsetI morphimS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)