1 files changed, 6 insertions, 0 deletions
diff --git a/peano.lisp b/peano.lisp
index 7d042f2..8fedc56 100644
--- a/peano.lisp
+++ b/peano.lisp
@@ -44,6 +44,12 @@
            (equal (nat= x y)
                   (equal x y))))
 
+(defmacro nat< (x y)
+  `(member-equal ,x ,y))
+
+(defthm nat<-succ
+  (nat< x (succ x)))
+
 (defun nat+ (x y)
   (if (z? y)
       x