diff options
author | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-06 00:42:10 +0900 |
---|---|---|
committer | Masaya Tojo <masaya@tojo.tokyo> | 2021-08-06 00:42:10 +0900 |
commit | e00735e48932889c2f78ecbcd84554aeaf913179 (patch) | |
tree | c380a78fe34909a4dc880e125f94a748e85c2f98 /peano.lisp | |
parent | a31c56c0051818cf8e952d0919eeefa05342e9f8 (diff) |
peano: Add nat+-right-cancellative theorem.
Diffstat (limited to 'peano.lisp')
-rw-r--r-- | peano.lisp | 7 |
1 files changed, 7 insertions, 0 deletions
@@ -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)))) |