REAL_ARITH : term -> thm
# REAL_ARITH `abs(x) < min e d / &2 /\ abs(y) < min e d / &2 ==> abs(x + y) < d + e`;; val it : thm = |- abs x < min e d / &2 /\ abs y < min e d / &2 ==> abs (x + y) < d + e
# REAL_ARITH `(&1 + x) * (&1 - x) * (&1 + x pow 2) < &1 ==> &0 < x pow 4`;; val it : thm = |- (&1 + x) * (&1 - x) * (&1 + x pow 2) < &1 ==> &0 < x pow 4