Lemmas about rational-listp available in the
Note: this book is extremely minimal. You should generally instead
see std/typed-lists/rational-listp. Note however that this book is part
of a widely-used library of basic arithmetic facts:
Theorem:
(defthm append-preserves-rational-listp (implies (true-listp x) (equal (rational-listp (append x y)) (and (rational-listp x) (rational-listp y)))))
Theorem:
(defthm rationalp-car-rational-listp (implies (and (rational-listp x) x) (rationalp (car x))) :rule-classes :forward-chaining)