)

let lemma05=MATCH_MP lemma03 lemma04;;
g`x = sqrt(&2) * y /\ ~(y = &0) ==> x * x = sqrt(&2) pow 2 * y * y /\ ~(y = &0)`;;
e(REPEAT STRIP_TAC);;
e(ASM_SIMP_TAC[REAL_MUL_AC; POW_2]);;
e(ASM_MESON_TAC[]);;
let lemma06=top_thm();;
(*
MESON[REAL_MUL_AC; POW_2]`x = sqrt(&2) * y /\ ~(y = &0) ==> x * x = sqrt(&2) pow 2 * y * y /\ ~(y = &0)`;; でも行けるが．．．
let lemma06=REAL_RING `x = sqrt(&2) * y /\ ~(y = &0) ==> x * x = sqrt(&2) pow 2 * y * y /\ ~(y = &0)`;;