proposition: Lemma morphpreIim R : f @*^-1 (f @* D :&: R) = f @*^-1 R.
proof: Proof. apply/setP=> x; rewrite morphimEdom !inE. by case Dx: (x \in D); rewrite // imset_f. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)