proposition: Lemma ifactmE : {in D, forall x, ifactm (f x) = g x}.
proof: Proof. rewrite /ifactm => x Dx; case: domP => f' /= [def_f' _ _ _]. by rewrite {f'}def_f' //= invmE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)