Built-in axioms and theorems about ordinals.
Theorem:
(defthm o-p-implies-o<g (implies (o-p a) (o<g a)))
Theorem:
(defthm acl2-count-car-cdr-linear (implies (consp x) (equal (acl2-count x) (+ 1 (acl2-count (car x)) (acl2-count (cdr x))))) :rule-classes :linear)