diff --git a/examples/lean/ex4.lean b/examples/lean/ex4.lean
new file mode 100644
index 000000000..827d98c8d
--- /dev/null
+++ b/examples/lean/ex4.lean
@@ -0,0 +1,6 @@
+Definition a : Nat := 10
+(* Trivial indicates a "proof by evaluation" *)
+Theorem T1 : a > 0 := Trivial
+Theorem T2 : a - 5 > 3 := Trivial
+(* The next one fails *)
+Theorem T3- : a > 11 := Trivial
\ No newline at end of file