proposition: Lemma morphim_ifactm (A : {set gT}) : A \subset D -> ifactm @* (f @* A) = g @* A.
proof: Proof. rewrite /ifactm => sAD; case: domP => _ /= [_ _ _ ->]. by rewrite morphim_comp morphim_invm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)