test: additional tests from issue #4413

leanprover · Jun 11, 2024 · 9a1cc13 · 9a1cc13
1 parent 98402c3
commit 9a1cc13
Showing 1 changed file with 22 additions and 0 deletions.
diff --git a/tests/lean/run/4413.lean b/tests/lean/run/4413.lean
@@ -25,3 +25,25 @@ set_option maxRecDepth 100 in
 set_option maxHeartbeats 100 in
 example (n : UInt64) : n = n - 1 :=
   rfl
+
+namespace Ex2
+
+def lowerSemitone := fun (n : Note) => Note.mk (n.1 - 0) n.2
+
+set_option maxRecDepth 100 in
+theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
+    0 ≤ (lowerSemitone n).start :=
+  (Nat.zero_le (Note.start n))
+
+end Ex2
+
+namespace Ex3
+
+def lowerSemitone := fun (n : Note) => Note.mk (n.1 + 100) n.2
+
+set_option maxRecDepth 200 in
+theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
+    0 ≤ (lowerSemitone n).start :=
+  (Nat.zero_le (Note.start n))
+
+end Ex3