Build_IsLeftSubmodule' {R : Ring} {M : LeftModule R} (H : M -> Type) `{forall x, IsHProp (H x)} (z : H zero) (c : forall r n m, H n -> H m -> H (n + r *L m)) : IsLeftSubmodule H. Proof. snrapply Build_IsLeftSubmodule. - snrapply Build_IsSubgroup'. + exact _. + exact z. + intros x y hx hy. change (sg_op ?x ?y) with (x + y). pose proof (p := c (-1) x y hx hy). rewrite lm_minus_one in p. exact p. - intros r m hm. rewrite <- (grp_unit_l). by apply c. 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.