proposition: Lemma morphpre_subcent1 R x : x \in D -> 'C_(f @*^-1 R)[x] \subset f @*^-1 'C_R[f x].
proof: Proof. move=> Dx; rewrite -morphpreIdom -setIA setICA morphpreI setIS //. exact: morphpre_cent1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)