From e00735e48932889c2f78ecbcd84554aeaf913179 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 6 Aug 2021 00:42:10 +0900
Subject: peano: Add nat+-right-cancellative theorem.

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

(limited to 'peano.lisp')

diff --git a/peano.lisp b/peano.lisp
index c25fbf3..138527b 100644
--- a/peano.lisp
+++ b/peano.lisp
@@ -93,3 +93,10 @@
            (equal (equal (nat+ k x) (nat+ k y))
                   (equal x y)))
   :hints (("Goal" :induct (nat= x y))))
+
+(defthm nat+-right-cancellative
+  (implies (and (nat? x)
+                (nat? y)
+                (nat? k))
+           (equal (equal (nat+ x k) (nat+ y k))
+                  (equal x y))))
-- 
cgit v1.2.3