peano: Rename theorems.

1 files changed, 15 insertions, 22 deletions

diff --git a/peano.lisp b/peano.lisp
index 791e04e..c25fbf3 100644
--- a/peano.lisp
+++ b/peano.lisp
@@ -68,32 +68,25 @@
            (equal (nat+ nil x)
                   x)))
 
-(defthm nat+-cancellative-1-1-1
-  (implies (and (consp x)
-                (nat? x)
-                (nat? k))
-           (not (equal (nat+ x k)
-                       k))))
+(defthm nat+-left-not-zp
+  (implies (and (nat? x)
+                (not (z? x))
+                (nat? y))
+           (not (equal (nat+ x y)
+                       y))))
 
-(defthm nat+-cancellative-1-1
-  (implies (and (consp x)
-                (nat? x)
-                (nat? k))
-           (not (equal (nat+ k x)
-                       k)))
+(defthm nat+-right-not-zp
+  (implies (and (nat? x)
+                (nat? y)
+                (not (z? y)))
+           (not (equal (nat+ x y)
+                       x)))
   :hints (("Goal" :in-theory (disable nat+-commutative)
                   :use ((:instance nat+-commutative
-                                    (x x)
-                                    (y k))))))
-
-(defthm nat+-cancellative-1
-  (implies (and (consp x)
-                (nat? x)
-                (nat? k))
-           (not (equal (nat+ k x)
-                       k))))
+                                   (x x)
+                                   (y y))))))
 
-(defthm nat+-cancellative
+(defthm nat+-left-cancellative
   (implies (and (nat? x)
                 (nat? y)
                 (nat? k))