Lemmas about

These are basic lemmas about:

BOZO these only address when A is positive and B/C are naturals. We should extend these to negative numbers.

**Theorem: **

(defthm |(< (ash a b) (ash a c))| (implies (and (posp a) (natp b) (natp c)) (equal (< (ash a b) (ash a c)) (< b c))))

**Theorem: **

(defthm |(= (ash a b) (ash a c))| (implies (and (posp a) (natp b) (natp c)) (equal (equal (ash a b) (ash a c)) (equal b c))))