rational-listp

(in-package "ACL2")

(defsection arithmetic/rational-listp
  :parents (rational-listp)
  :short "Lemmas about @(see rational-listp) available in the
@('arithmetic/rational-listp') book."
  :long "<p>Note: this book is extremely minimal.  You should generally instead
see @(see std/typed-lists/rational-listp).  Note however that this book is part
of a widely-used library of basic arithmetic facts: @('(include-book
"arithmetic/top" :dir :system)').</p>"
  (defthm append-preserves-rational-listp
    (implies (true-listp x)
      (equal (rational-listp (append x y))
        (and (rational-listp x) (rational-listp y)))))
  (defthm rationalp-car-rational-listp
    (implies (and (rational-listp x) x) (rationalp (car x)))
    :rule-classes :forward-chaining))