2 (`!p q. p * p = 2 * q * q ==> q = 0`,
3 MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
4 REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN
5 REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
6 DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
7 FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN
8 ASM_REWRITE_TAC[ARITH_RULE
9 `q < 2 * m ==> q * q = 2 * m * m ==> m = 0 <=>
10 (2 * m) * 2 * m = 2 * q * q ==> 2 * m <= q`] THEN
11 ASM_MESON_TAC[LE_MULT2; MULT_EQ_0; ARITH_RULE `2 * x <= x <=> x = 0`]);;