Lemmas for the bounds of
These are lemmas for:
BOZO these only address when A is positive. We should extend these to negative numbers.
(defthm |(< a (ash a b)) when (posp a)| (implies (posp a) (equal (< a (ash a b)) (posp b))) :rule-classes ((:rewrite) (:linear :corollary (implies (and (posp a) (posp b)) (< a (ash a b))))))