proposition: Lemma morphpre_inj : {in [pred R : {set rT} | R \subset f @* D] &, injective (fun R => f @*^-1 R)}.
proof: Proof. exact: can_in_inj morphpreK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)