We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 727d552 commit 0f28c6cCopy full SHA for 0f28c6c
tests/lean/run/grind_proof_perf_issue.lean
@@ -1,2 +1,6 @@
1
example {n : Nat} (hn : 500000 ≤ n) (hn' : n ≤ 2000000) : n - 500000 ≥ 1500001 → False := by
2
grind
3
+
4
+example {n : Nat} (hn : 57343 < n) (hn' : n < 1114112) :
5
+ n - (57343 + 1) < 1114111 - 57343 := by
6
+ grind
0 commit comments