{R : Ring} : LeftModule R -> LeftModule R -> LeftModule R. Proof. intros M N. snrapply (Build_LeftModule R (ab_biprod M N)). snrapply Build_IsLeftModule. - intros r. apply functor_prod; exact (lact r). - intros r m n. apply path_prod; apply lm_dist_l. - intros r m n. apply path_prod; apply lm_dist_r. - intros r s m. apply path_prod; apply lm_assoc. - intros r. apply path_prod; apply lm_unit. Defined.
Require Import WildCat. Require Import Spaces.Nat.Core. Require Import Classes.interfaces.canonical_names. Require Import Algebra.Groups.Kernel Algebra.Groups.Image Algebra.Groups.QuotientGroup. Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct. Require Import Rings.Ring.