		Search-engine friendly clone of the ACL2 documentation.

Library-extensions

Arithmetic-theorems

Some theorems about arithmetic.

Definitions and Theorems

Theorem: evenp-of-1-less-when-not-evenp

(defthm evenp-of-1-less-when-not-evenp
  (implies (and (integerp x) (not (evenp x)))
           (evenp (1- x))))

Theorem: evenp-of-3-less-when-not-evenp

(defthm evenp-of-3-less-when-not-evenp
  (implies (and (integerp x) (not (evenp x)))
           (evenp (- x 3))))

Theorem: lt-to-2+le-when-both-evenp

(defthm lt-to-2+le-when-both-evenp
  (implies (and (rationalp x)
                (rationalp y)
                (evenp x)
                (evenp y))
           (equal (< x y) (<= (+ 2 x) y))))