proposition: Lemma islinearfuncomp {R : ring} {M N P : module R} (f : linearfun M N) (g : linearfun N P) : islinear (funcomp f g).
proof: Proof. intros r x; simpl. rewrite (linearfun_islinear f). rewrite (linearfun_islinear g). apply idpath. Defined.
imports: UniMath.MoreFoundations.Tactics UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.Monoids