∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : PartialOrder M] [inst_4 : SMulWithZero R M] [hM : IsOrderedModule R M], IsOrderedModule { c // 0 ≤ c } M