chore: updates to (failing) grind algebra tests (#8987)

tests/lean/grind/algebra/nat.lean

@@ -5,7 +5,8 @@ variable [CommRing R] [LinearOrder R] [OrderedRing R]
 example (a b : R) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
 example (a b : R) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
 
--- These should work by specializing `R` to `Int`!
+-- These don't work because `cutsat` disables `linarith`.
+-- We could use the CommRing normalizer in cutsat to solve these.
 example (a b : Int) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
 example (a b : Int) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
 

tests/lean/grind/algebra/nat_module.lean

@@ -6,7 +6,7 @@ variable (M : Type) [IntModule M]
 
 example (x y : M) : 2 * x + 3 * y + x = 3 * (x + y) := by grind
 
-variable [LinearOrder M]
+variable [LinearOrder M] [OrderedAdd M]
 
 example {x y : M} (h : x ≤ y) : 2 * x + y ≤ 3 * y := by grind
 
@@ -19,7 +19,7 @@ variable (M : Type) [NatModule M]
 
 example (x y : M) : 2 * x + 3 * y + x = 3 * (x + y) := by grind
 
-variable [LinearOrder M]
+variable [LinearOrder M] [OrderedAdd M]
 
 example {x y : M} (h : x ≤ y) : 2 * x + y ≤ 3 * y := by grind
 

tests/lean/grind/algebra/nlinarith.lean

@@ -1,5 +1,7 @@
 open Lean.Grind
 
+-- TODO which other systems, e.g. Mathematica, Isabelle, nlia, can handle these?
+
 variable (R : Type) [CommRing R] [LinearOrder R] [OrderedRing R]
 
 example (a : R) : 0 ≤ a^2 := by grind