Basic ordering facts about
Theorem:
(defthm char<-irreflexive (equal (char< x x) nil))
Theorem:
(defthm char<-antisymmetric (implies (char< x y) (not (char< y x))))
Theorem:
(defthm char<-transitive (implies (and (char< x y) (char< y z)) (char< x z)))
Theorem:
(defthm char<-trichotomy-weak (implies (and (not (char< x y)) (not (char< y x))) (equal (chareqv x y) t)))
Theorem:
(defthm char<-trichotomy-strong (equal (char< x y) (and (not (chareqv x y)) (not (char< y x)))) :rule-classes ((:rewrite :loop-stopper ((x y)))))