proposition: Lemma morphpreK R : R \subset f @* D -> f @* (f @*^-1 R) = R.
proof: Proof. move=> sRfD; apply/setP=> y; apply/morphimP/idP=> [[x _] | Ry]. by rewrite !inE; case/andP=> _ Rfx ->. have /morphimP[x Dx _ defy]: y \in f @* D := subsetP sRfD y Ry. by exists x; rewrite // !inE Dx -defy. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)