Example (19)

今回は平方根を含む不等式の変形です．

g`!x y :real. &0 <= x ==> ( y <= sqrt x <=> y < &0 \/ (&0 <= y /\ y pow 2 <= x) )`;;
e(REPEAT STRIP_TAC);;
e(MP_TAC((UNDISCH o SPEC_ALL)SQRT_POS_LE));;
e(ABBREV_TAC`z = sqrt x`);;
e(ONCE_ASM_REWRITE_TAC[(UNDISCH o SPEC_ALL o GSYM)SQRT_POW_2] 
  THEN ASM_SIMP_TAC[]);;
e(CONV_TAC REAL_SOS);;