proposition: Lemma modulehombinop_ismodulefun {R : ring} {M N : module R} (f g : R-mod(M, N)) : @ismodulefun R M N (λ x : pr1 M, (pr1 f x * pr1 g x)%multmonoid).
proof: Proof. use make_ismodulefun. - exact (pr1 (abmonoidshombinop_ismonoidfun (modulefun_to_monoidfun f) (modulefun_to_monoidfun g))). - intros r m. rewrite (modulefun_to_islinear f). rewrite (modulefun_to_islinear g). rewrite <- module_mult_is_ldistr. reflexivity. Defined.
imports: UniMath.MoreFoundations.Tactics UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.Monoids