From 3d0dc785b63534feb515d3b8eb8dbb25abbfaced Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sat, 7 Aug 2021 15:13:20 +0900
Subject: peano: Add nat< function.

---
 peano.lisp | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'peano.lisp')

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
-- 
cgit v1.2.3