proposition: Lemma sub_morphpre_injm R A : A \subset D -> R \subset f @* D -> (f @*^-1 R \subset A) = (R \subset f @* A).
proof: Proof. by move=> sAD sRfD; rewrite -morphpreSK ?injmK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)