let REAL_RING =
let REAL_INTEGRAL = prove
(`(!x. &0 * x = &0) /\
(!x y z. (x + y = x + z) <=> (y = z)) /\
(!w x y z. (w * y + x * z = w * z + x * y) <=> (w = x) \/ (y = z))`,
REWRITE_TAC[MULT_CLAUSES; EQ_ADD_LCANCEL] THEN
REWRITE_TAC[GSYM REAL_OF_NUM_EQ;
GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
REWRITE_TAC[GSYM REAL_ENTIRE] THEN REAL_ARITH_TAC)
and REAL_INVERSE = prove
(`!x y:real. ~(x = y) <=> ?z. (x - y) * z = &1`,
REPEAT GEN_TAC THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM REAL_SUB_0] THEN
MESON_TAC[REAL_MUL_RINV; REAL_MUL_LZERO; REAL_ARITH `~(&1 = &0)`]) in
RING(rat_of_term,term_of_rat,REAL_RAT_EQ_CONV,
`(--):real->real`,`(+):real->real->real`,`(-):real->real->real`,
`(inv):real->real`,`(*):real->real->real`,`(/):real->real->real`,
`(pow):real->num->real`,
REAL_INTEGRAL,REAL_INVERSE,REAL_POLY_CONV);;
after which, for example, we can verify a reduction for cubic
equations to quadratics entirely automatically: