Theorem: logcdr-<-0
(defthm logcdr-<-0 (equal (< (logcdr i) 0) (and (integerp i) (< i 0))))
Theorem: justify-logcdr-induction
(defthm justify-logcdr-induction (and (implies (> i 0) (< (logcdr i) i)) (implies (< i -1) (< i (logcdr i)))))
