Support for NatModule in the grind linear arithmetic module.

theorem Lean.Grind.IntModule.OfNatModule.of_eq {α : Type u_1} [NatModule α] {a b : α} {a' b' : Q α} (h₁ : toQ a = a') (h₂ : toQ b = b') : a = b → a' = b'

theorem Lean.Grind.IntModule.OfNatModule.of_diseq {α : Type u_1} [NatModule α] [AddRightCancel α] {a b : α} {a' b' : Q α} (h₁ : toQ a = a') (h₂ : toQ b = b') : a ≠ b → a' ≠ b'

theorem Lean.Grind.IntModule.OfNatModule.of_le {α : Type u_1} [NatModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] {a b : α} {a' b' : Q α} (h₁ : toQ a = a') (h₂ : toQ b = b') : a ≤ b → a' ≤ b'

theorem Lean.Grind.IntModule.OfNatModule.of_not_le {α : Type u_1} [NatModule α] [LE α] [Std.IsPreorder α] [OrderedAdd α] {a b : α} {a' b' : Q α} (h₁ : toQ a = a') (h₂ : toQ b = b') : ¬a ≤ b → ¬a' ≤ b'

theorem Lean.Grind.IntModule.OfNatModule.of_lt {α : Type u_1} [NatModule α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedAdd α] {a b : α} {a' b' : Q α} (h₁ : toQ a = a') (h₂ : toQ b = b') : a < b → a' < b'

theorem Lean.Grind.IntModule.OfNatModule.of_not_lt {α : Type u_1} [NatModule α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedAdd α] {a b : α} {a' b' : Q α} (h₁ : toQ a = a') (h₂ : toQ b = b') : ¬a < b → ¬a' < b'

theorem Lean.Grind.IntModule.OfNatModule.add_congr {α : Type u_1} [NatModule α] {a b : α} {a' b' : Q α} (h₁ : toQ a = a') (h₂ : toQ b = b') : toQ (a + b) = a' + b'

theorem Lean.Grind.IntModule.OfNatModule.smul_congr {α : Type u_1} [NatModule α] (n : Nat) (a : α) (a' : Q α) (h : toQ a = a') : toQ (n • a) = n • a'