proposition: Lemma morphimMr A B : B \subset D -> f @* (A * B) = f @* A * f @* B.
proof: Proof. move=> sBD; apply: invg_inj. by rewrite invMg -!morphimV invMg morphimMl // -invGid invSg. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)