peano: Add nat+-right-cancellative theorem.

1 files changed, 7 insertions, 0 deletions

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))))