less-than

(in-package "ACL2")

(defthmd <-when-rationalp-and-complex-rationalp
  (implies (and (complex-rationalp y) (rationalp x))
    (equal (< x y)
      (if (< x (realpart y))
        t
        (and (equal x (realpart y)) (< 0 (imagpart y))))))
  :hints (("Goal" :use completion-of-<)))

(defthmd <-when-complex-rationalp-and-rationalp
  (implies (and (complex-rationalp x) (rationalp y))
    (equal (< x y)
      (if (< (realpart x) y)
        t
        (and (equal y (realpart x)) (< (imagpart x) 0)))))
  :hints (("Goal" :use completion-of-<)))

(defthmd <-when-complex-rationalp-and-complex-rationalp
  (implies (and (complex-rationalp y) (complex-rationalp x))
    (equal (< x y)
      (if (< (realpart x) (realpart y))
        t
        (and (equal (realpart x) (realpart y))
          (< (imagpart x) (imagpart y))))))
  :hints (("Goal" :use completion-of-<)))

(defthm not-<-same (not (< x x)))