From 076d7f8a9ac69f12e2014832bca65ea521a8e950 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 12 Jan 2025 20:17:11 -0800
Subject: [PATCH] test: from Kim's test suite

---
 tests/lean/run/grind_t1.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
index 1752266b8e31..d660f51b09d3 100644
--- a/tests/lean/run/grind_t1.lean
+++ b/tests/lean/run/grind_t1.lean
@@ -263,3 +263,9 @@ a✝ : p
 set_option trace.grind.split true in
 example (p q : Prop) : ¬(p ↔ q) → p → False := by
   grind -- should not split on (p ↔ q)
+
+example {a b : Nat} (h : a < b) : ¬ b < a := by
+  grind
+
+example {m n : Nat} : m < n ↔ m ≤ n ∧ ¬ n ≤ m := by
+  grind