anchor.diff:                     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)
  +   #else
  +     Sequent([],parse_term @"(!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))")
  +   #endif
      let REAL_RABINOWITSCH = 
         prove ((parse_term @"!x y:real. ~(x = y) <=> ?z. (x - y) * z = &1"),
           REPEAT GEN_TAC |>THEN<|
  
positive.code: // real_ideal_cofactors: Produces cofactors proving that one real polynomial is in the ideal generated by others.
  let REAL_RING,real_ideal_cofactors =
     let REAL_INTEGRAL = 
       prove ((parse_term @"(!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))"),
  
negative.code:          |> THEN <| MATCH_MP_TAC lemma
           |> THEN <| MATCH_MP_TAC REAL_LT_INV
           |> THEN <| ASM_REWRITE_TAC [])
  #else
      Sequent([],parse_term @"&0 < y1 /\ &0 < y2 ==> (x1 / y1 <= x2 / y2 <=> x1 * y2 <= x2 * y1)")
  #endif
  
  let RAT_LEMMA5 = 
      prove
  