chore: add grind test

2026-04-05 11:44:06 +00:00 · 2025-10-26 22:12:09 +11:00
1 changed files with 4 additions and 0 deletions
--- a/tests/lean/run/grind_ordered_ring.lean
+++ b/tests/lean/run/grind_ordered_ring.lean
@@ -0,0 +1,4 @@
+example {R : Type} [Lean.Grind.CommRing R] [LE R] [LT R]
+    [Std.LawfulOrderLT R] [Std.IsLinearOrder R] [Lean.Grind.OrderedRing R]
+    (x y z : R) (k l : Nat) :
+    x * y * z^(k + l) ≤ x * y * z^ k * z^l := by grind