diff --git a/src/Init/Grind/Module/Envelope.lean b/src/Init/Grind/Module/Envelope.lean
index 03745526ad..69ac854324 100644
--- a/src/Init/Grind/Module/Envelope.lean
+++ b/src/Init/Grind/Module/Envelope.lean
@@ -318,6 +318,29 @@ instance [LE α] [IsPreorder α] [OrderedAdd α] : IsPreorder (OfNatModule.Q α)
     rw [this]; clear this
     exact OrderedAdd.add_le_add h₁ h₂
 
+instance [LE α] [IsPartialOrder α] [OrderedAdd α] : IsPartialOrder (OfNatModule.Q α) where
+  le_antisymm a b h₁ h₂ := by
+    induction a using Q.ind with | _ a
+    induction b using Q.ind with | _ b
+    rcases a with ⟨a₁, a₂⟩; rcases b with ⟨b₁, b₂⟩
+    simp only [mk_le_mk] at h₁ h₂
+    rw [AddCommMonoid.add_comm b₁ a₂, AddCommMonoid.add_comm b₂ a₁] at h₂
+    have := IsPartialOrder.le_antisymm _ _ h₁ h₂
+    apply Quot.sound
+    simp; exists 0
+    rw [this]
+
+instance [LE α] [IsLinearPreorder α] [OrderedAdd α] : IsLinearPreorder (OfNatModule.Q α) where
+  le_total a b := by
+    induction a using Q.ind with | _ a
+    induction b using Q.ind with | _ b
+    rcases a with ⟨a₁, a₂⟩; rcases b with ⟨b₁, b₂⟩
+    simp only [mk_le_mk]
+    rw [AddCommMonoid.add_comm b₁ a₂, AddCommMonoid.add_comm b₂ a₁]
+    apply le_total
+
+instance [LE α] [IsLinearOrder α] [OrderedAdd α] : IsLinearOrder (OfNatModule.Q α) where
+
 attribute [-simp] Q.mk
 
 @[local simp] private theorem mk_lt_mk