proposition: Lemma morphpre_subcent R A : 'C_(f @*^-1 R)(A) \subset f @*^-1 'C_R(f @* A).
proof: Proof. by rewrite -morphpreIdom -setIA setICA morphpreI setIS //; apply: morphpre_cent. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)