proposition: Lemma morphpre_cents A R : R \subset f @* D -> f @*^-1 R \subset 'C(A) -> R \subset 'C(f @* A).
proof: Proof. by move=> sRfD; move/morphim_cents; rewrite morphpreK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)