{R : Ring} {M : RightModule R} (H : M -> Type) `{forall x, IsHProp (H x)} (z : H zero) (c : forall r n m, H n -> H m -> H (n + m *R r)) : RightSubmodule M := Build_LeftSubmodule' (R:=rng_op R) H z c.
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.