Ordered instances on submodules

instance Submodule.toIsOrderedAddMonoid {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [Module R M] (S : Submodule R M) : IsOrderedAddMonoid ↥S

A submodule of an ordered additive monoid is an ordered additive monoid.

instance Submodule.toIsOrderedCancelAddMonoid {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [Module R M] (S : Submodule R M) : IsOrderedCancelAddMonoid ↥S

A submodule of an ordered cancellative additive monoid is an ordered cancellative additive monoid.