proposition: Lemma morphpre_ifactm C : ifactm @*^-1 C = f @* (g @*^-1 C).
proof: Proof. rewrite /ifactm; case: domP => _ /= [_ _ -> _]. by rewrite morphpre_comp morphpre_invm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)