$$$sqrt2.pvs
SQRT2 : THEORY
BEGIN

  reals : LIBRARY = "/usr/local/share/pvslib/reals"

  IMPORTING reals@sqrt

  even_or_odd : LEMMA
    FORALL(n:nat) : even?(n) XOR odd?(n)

  square_even_odd : LEMMA
    FORALL(n:nat) : (even?(n) IMPLIES even?(n*n))
                      AND
                    (odd?(n) IMPLIES odd?(n*n))

  sqrt2 : LEMMA
    FORALL(n,m:nat) : n>0 IMPLIES NOT n*n = 2*m*m

% Non-rationality result.
% Note that rational? is introduced *axiomatically* in the prelude,
% and therefore not useable here.

  Rational? : PRED[real] =
    { t : real | EXISTS(n:int, m:posnat) : t = n/m }
  
  sqrt2_non_rational : LEMMA
    NOT Rational?(sqrt(2))
    
END SQRT2

$$$sqrt2.prf
(SQRT2
 (|even_or_odd| "" (INDUCT-AND-SIMPLIFY "n" :IF-MATCH NIL)
  (("" (INST 2 "j!2+1") (("" (ASSERT) NIL NIL)) NIL)) NIL)
 (|square_even_odd| "" (INDUCT-AND-SIMPLIFY "n" :IF-MATCH NIL)
  (("1" (INST 2 "j!3+j!1") (("1" (ASSERT) NIL NIL)) NIL)
   ("2" (INST 2 "1+j!2+j!1") (("2" (ASSERT) NIL NIL)) NIL)
   ("3" (INST 2 "j!2-1") (("3" (ASSERT) NIL NIL)) NIL))
  NIL)
 (|sqrt2| "" (INDUCT "n" :NAME "NAT_induction")
  (("" (SKOSIMP*)
    (("" (USE "even_or_odd")
      (("" (EXPAND* "XOR" "/=")
        (("" (BDDSIMP)
          (("1" (EXPAND "even?")
            (("1" (SKOSIMP*)
              (("1" (INST -2 "m!1")
                (("1" (GROUND)
                  (("1" (INST -1 "j!2")
                    (("1" (LEMMA "nonzero_times3")
                      (("1" (GRIND :IF-MATCH ALL) NIL NIL)) NIL))
                    NIL)
                   ("2" (LEMMA "gt_times_gt_pos1")
                    (("2" (INST -1 "j!1" "j!1" "m!1" "m!1")
                      (("2" (ASSERT)
                        (("2" (LEMMA "pos_times_gt")
                          (("2" (GRIND :IF-MATCH ALL) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (USE "square_even_odd") (("2" (GRIND) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|sqrt2_non_rational| "" (EXPAND "Rational?")
  (("" (SKOSIMP)
    (("" (LEMMA "sqrt2")
      (("" (INST - "abs(n!1)" "abs(m!1)")
        (("" (CASE-REPLACE "n!1*n!1=2*m!1*m!1")
          (("1" (GRIND) NIL NIL)
           ("2" (USE "sqrt_def")
            (("2" (GRIND)
              (("2" (USE "div_cancel3") (("2" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))