anchor.diff:      prove((parse_term @"!x y. (--x) - (--y) = y - x"), REAL_ARITH_TAC)
   let REAL_SUB_TRIANGLE = 
       prove((parse_term @"!a b c. (a - b) + (b - c) = a - c"), REAL_ARITH_TAC)
  +
   let REAL_EQ_SUB_LADD = 
  +#if BUGGY
       prove((parse_term @"!x y z. (x = y - z) <=> (x + z = y)"), REAL_ARITH_TAC)
  +#else
  +    Sequent([],parse_term @"!x y z. (x = y - z) <=> (x + z = y)")
  +#endif
  +
   let REAL_EQ_SUB_RADD = 
  +#if BUGGY
       prove((parse_term @"!x y z. (x - y = z) <=> (x = z + y)"), REAL_ARITH_TAC)
  +#else
  +    Sequent([],parse_term @"!x y z. (x - y = z) <=> (x = z + y)")
  +#endif
  +
  +
   let REAL_SUB_SUB2 = prove((parse_term @"!x y. x - (x - y) = y"), REAL_ARITH_TAC)
   let REAL_ADD_SUB2 = 
       prove((parse_term @"!x y. x - (x + y) = --y"), REAL_ARITH_TAC)
  +
   let REAL_EQ_IMP_LE = 
  +#if BUGGY
       prove((parse_term @"!x y. (x = y) ==> x <= y"), REAL_ARITH_TAC)
  -let REAL_POS_NZ = prove((parse_term @"!x. &0 < x ==> ~(x = &0)"), REAL_ARITH_TAC)
  +#else
  +    Sequent([],parse_term @"!x y. (x = y) ==> x <= y")
  +#endif
  +
  +let REAL_POS_NZ = 
  +#if BUGGY
  +    prove((parse_term @"!x. &0 < x ==> ~(x = &0)"), REAL_ARITH_TAC)
  +#else
  +    Sequent([],parse_term @"!x. &0 < x ==> ~(x = &0)")
  +#endif
  +
   let REAL_DIFFSQ = 
       prove
           ((parse_term @"!x y. (x + y) * (x - y) = (x * x) - (y * y)"), 
            REAL_ARITH_TAC)
  +
   let REAL_EQ_NEG2 = 
  +#if BUGGY
       prove((parse_term @"!x y. (--x = --y) <=> (x = y)"), REAL_ARITH_TAC)
  +#else
  +    Sequent([],parse_term @"!x y. (--x = --y) <=> (x = y)")
  +#endif
  +
   let REAL_LT_NEG2 = 
       prove((parse_term @"!x y. --x < --y <=> y < x"), REAL_ARITH_TAC)
   let REAL_SUB_LDISTRIB = 
  
positive.code:          REWRITE_TAC [REAL_POW_2; REAL_LE_SQUARE])
  
  let REAL_SOS_EQ_0 = 
      prove
          ((parse_term @"!x y. x pow 2 + y pow 2 = &0 <=> x = &0 /\ y = &0"), 
           REPEAT GEN_TAC
  
negative.code:          MESON_TAC [REAL_MUL_SYM; REAL_LT_LMUL])
  
  let REAL_EQ_MUL_LCANCEL = 
  #if BUGGY
      prove
          ((parse_term @"!x y z. (x * y = x * z) <=> (x = &0) \/ (y = z)"), 
           REPEAT GEN_TAC
  