Theorem: bitp-mod-2
(defthm bitp-mod-2 (implies (integerp i) (bitp (mod i 2))) :rule-classes ((:rewrite) (:generalize :corollary (implies (integerp i) (or (equal (mod i 2) 0) (equal (mod i 2) 1))))))
