proposition: Lemma morphpre_restrm R : fA @*^-1 R = A :&: f @*^-1 R.
proof: Proof. by rewrite setIA (setIidPl sAD). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)