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