Build_LeftSubmodule' {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)) : LeftSubmodule M. Proof. pose (p := Build_IsLeftSubmodule' H z c). snrapply Build_LeftSubmodule. 1: snrapply (Build_Subgroup _ H). 2: exact p. rapply ils_issubgroup. 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.