Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v
new file mode 100644
index 00000000..d3e98ae4
--- /dev/null
+++ b/test-suite/modules/Nat.v
@@ -0,0 +1,19 @@
+Definition T:=nat.
+
+Definition le:=Peano.le.
+
+Hints Unfold le.
+
+Lemma le_refl:(n:nat)(le n n).
+  Auto.
+Qed.
+
+Require Le.
+
+Lemma le_trans:(n,m,k:nat)(le n m) -> (le m k) -> (le n k).
+  EAuto with arith.
+Qed.
+
+Lemma le_antis:(n,m:nat)(le n m) -> (le m n) -> n=m.
+  EAuto with arith.
+Qed.