proposition: Lemma morphpreMr R S : S \subset f @* D -> f @*^-1 (R * S) = f @*^-1 R * f @*^-1 S.
proof: Proof. move=> sSfD; apply: invg_inj. by rewrite invMg -!morphpreV invMg morphpreMl // -invSg invgK invGid. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)