; Arithmetic can be surprisingly tough to reason about, but let's ; give it a try: (defun sum-up-to (n) (if (zp n) 0 (+ n (sum-up-to (1- n))))) (sum-up-to 4) (defthm sum-up-to-property ; fails (implies (natp n) (equal (sum-up-to n) (/ (* n (+ 1 n)) 2)))) (include-book "arithmetic/top" :dir :system) (defthm sum-up-to-property (implies (natp n) (equal (sum-up-to n) (/ (* n (+ 1 n)) 2)))) ; Better yet: :ubt! :x-1 ; undo defthm and include-book (encapsulate () (local (include-book "arithmetic/top" :dir :system)) (defthm sum-up-to-property (implies (natp n) (equal (sum-up-to n) (/ (* n (+ 1 n)) 2)))))