let thm20120112=prove
(`~(?x y. &x / &y = sqrt (&2) )`,
REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o (MATCH_MP lemma08)) THEN
SIMP_TAC[REAL_MUL; REAL_INJ] THEN
MESON_TAC[thm20120110_2]);;
0..0..1..solved at 4
val thm20120112 : thm = |- ~(?x y. &x / &y = sqrt (&2))