proposition: Lemma modulehombinop_inv_ismodulefun {R : ring} {M N : module R} (f : R-mod(M, N)) : ismodulefun (λ m : M, grinv N (pr1 f m)).
proof: Proof. use tpair. - use make_isbinopfun. intros x x'. cbn. rewrite (pr1 (pr2 f)). rewrite (pr2 (pr2 (pr1module N))). use (grinvop N). - intros r m. rewrite <- module_inv_mult. apply maponpaths. apply (pr2 f). Qed.
imports: UniMath.MoreFoundations.Tactics UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.Monoids