proposition: Lemma unelmodulefun_ismodulefun {R : ring} (M N : module R) : ismodulefun (λ x : M, (unel N)).
proof: Proof. use make_ismodulefun. - use make_isbinopfun. intros m m'. use pathsinv0. use lunax. - intros r m. rewrite module_mult_1. reflexivity. Qed.
imports: UniMath.MoreFoundations.Tactics UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.Monoids