proposition: Lemma mem_morphpre R x : x \in D -> f x \in R -> x \in f @*^-1 R.
proof: Proof. by move=> Dx Rfx; apply/morphpreP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)