(in-package "ACL2")

(include-book "/u/acl2/v6/acl2/current/books/rtl/rel4/lib/arith")

(defun induction-scheme (m n)
  (declare (xargs :measure (+ (nfix m) (nfix n))))
  (if (and (not (zp m)) (not (zp n)) (= (* m m) (* 2 n n)))
      (induction-scheme (- (* 2 n) m) (- m n))
    t))

(defthm lemma-1
    (implies (and (not (zp m)) (not (zp n)))
	     (not (= (* m m) (* 2 n n))))
  :hints (("Goal" :induct (induction-scheme m n))))

(defthm lemma-2
    (implies (and (integerp m) (not (zp n)))
	     (not (= (* (/ m n) (/ m n)) 2)))
  :hints (("Goal" :use (lemma-1
			(:instance lemma-1 (m (- m)))
			(:instance cancel-equal-* (r (* M M (/ N) (/ N))) (s 2) (a (* n n)))))))

(defthm sqrt2-irrational
    (implies (rationalp x)
	     (not (= (* x x) 2)))
  :hints (("Goal" :use (:instance lemma-2 (m (numerator x)) (n (denominator x))))))