let lem1 = SIMP_RULE [REAL_POW2_ABS; REAL_INJ; REAL_MUL]
(REAL_FIELD `~(&q = &0) ==> abs x = &p / &q ==> ~(&(gcd (p,q)) = &0)
==> &p = &a' * &(gcd (p,q)) ==> &q = &b' * &(gcd (p,q))
==> &a' * &a' = abs x pow 2 * &b' * &b'`);;
let RATIONAL_COPRIME = prove
(`!x. rational x ==> (?p q. &p * &p = x pow 2 * &q * &q /\ coprime (p,q))`,
SIMP_TAC [RATIONAL_ALT] THEN REPEAT STRIP_TAC THEN
ASM_PV9_TAC [GCD_ZERO; GCD_COPRIME_EXISTS; REAL_MUL; lem1]);;
let RATIONAL_SQRT = prove
(`!m. rational (sqrt (&m)) <=> (?n. m = n * n)`,
GEN_TAC THEN EQ_TAC THENL
[DISCH_THEN (MP_TAC o (MATCH_MP RATIONAL_COPRIME)) THEN
SIMP_TAC [REAL_POS; SQRT_POW_2; REAL_MUL; REAL_INJ] THEN STRIP_TAC THEN
ASM_PV9_TAC [PRIME_FACTOR; DIVIDES_LMUL; PRIME_DIVPROD; coprime; prime;
MULT_CLAUSES];
PV9_TAC ([GSYM REAL_MUL; GSYM POW_2; REAL_POS; POW_2_SQRT] @
[rational; INTEGER_CLOSED;
REAL_FIELD` ~(&1 = &0) /\ &n = &n / &1`])]);;
let PRIME_NOT_SQUARE = prove
(`!s. prime s ==> ~(?n. s = n * n)`,
REPEAT STRIP_TAC THEN
SUBGOAL_TAC "" `n = 1 \/ n = s` [ASM_MESON_TAC[divides; prime]] THEN
SUBGOAL_THEN `s = 0 \/ s = 1` ASSUME_TAC THENL
[MAP_EVERY GET_TAC [2;1] THEN CONV_TAC NUM_RING; ASM_MESON_TAC[PRIME]]);;
let SQRT_PRIME_NOT_RATIONAL = SIMP_RULE [GSYM RATIONAL_SQRT] PRIME_NOT_SQUARE;;
