anchor.diff:           |> THEN <| REAL_ARITH_TAC)
   
   let REAL_SGN_INV = 
  -    prove
  -        ((parse_term @"!x. real_sgn(inv x) = real_sgn x"), 
  -         REWRITE_TAC [real_sgn
  -                      REAL_LT_INV_EQ
  -                      GSYM REAL_INV_NEG
  -                      REAL_ARITH(parse_term @"x < &0 <=> &0 < --x")])
  +    prove((parse_term @"!x. real_sgn(inv x) = real_sgn x"), 
  +          REWRITE_TAC [real_sgn;
  +                       REAL_LT_INV_EQ;
  +                       GSYM REAL_INV_NEG;
  +                       REAL_ARITH(parse_term @"x < &0 <=> &0 < --x")])
   
   let REAL_SGN_DIV = 
       prove
  
positive.code: 
  let REAL_NOT_LE = 
      prove((parse_term @"!x y. ~(x <= y) <=> y < x"), REAL_ARITH_TAC)
  let REAL_LET_ANTISYM = 
      prove((parse_term @"!x y. ~(x <= y /\ y < x)"), REAL_ARITH_TAC)
  let REAL_NEG_LT0 = 
      prove((parse_term @"!x. (--x) < &0 <=> &0 < x"), REAL_ARITH_TAC)
  let REAL_NEG_GT0 = 
      prove((parse_term @"!x. &0 < (--x) <=> x < &0"), REAL_ARITH_TAC)
  let REAL_NEG_LE0 = 
      prove((parse_term @"!x. (--x) <= &0 <=> &0 <= x"), REAL_ARITH_TAC)
  let REAL_NEG_GE0 = 
      prove((parse_term @"!x. &0 <= (--x) <=> x <= &0"), REAL_ARITH_TAC)
  let REAL_LT_TOTAL = 
      prove((parse_term @"!x y. (x = y) \/ x < y \/ y < x"), REAL_ARITH_TAC)
  let REAL_LT_NEGTOTAL = 
      prove((parse_term @"!x. (x = &0) \/ (&0 < x) \/ (&0 < --x)"), REAL_ARITH_TAC)
  let REAL_LE_01 = prove((parse_term @"&0 <= &1"), REAL_ARITH_TAC)
  let REAL_LT_01 = prove((parse_term @"&0 < &1"), REAL_ARITH_TAC)
  let REAL_LE_LADD = 
      prove((parse_term @"!x y z. (x + y) <= (x + z) <=> y <= z"), REAL_ARITH_TAC)
  let REAL_LE_RADD = 
      prove((parse_term @"!x y z. (x + z) <= (y + z) <=> x <= y"), REAL_ARITH_TAC)
  let REAL_LT_ADD2 = 
      prove
          ((parse_term @"!w x y z. w < x /\ y < z ==> (w + y) < (x + z)"), 
           REAL_ARITH_TAC)
  let REAL_LE_ADD2 = 
      prove
          ((parse_term @"!w x y z. w <= x /\ y <= z ==> (w + y) <= (x + z)"), 
           REAL_ARITH_TAC)
  let REAL_LT_LNEG = 
      prove
          ((parse_term @"!x y. --x < y <=> &0 < x + y"), 
           REWRITE_TAC [real_lt; REAL_LE_RNEG; REAL_ADD_AC])
  let REAL_LT_RNEG = 
      prove
          ((parse_term @"!x y. x < --y <=> x + y < &0"), 
           REWRITE_TAC [real_lt; REAL_LE_LNEG; REAL_ADD_AC])
  let REAL_LT_ADDNEG = 
      prove
          ((parse_term @"!x y z. y < (x + (--z)) <=> (y + z) < x"), REAL_ARITH_TAC)
  let REAL_LT_ADDNEG2 = 
      prove
          ((parse_term @"!x y z. (x + (--y)) < z <=> x < (z + y)"), REAL_ARITH_TAC)
  let REAL_LT_ADD1 = 
      prove((parse_term @"!x y. x <= y ==> x < (y + &1)"), REAL_ARITH_TAC)
  let REAL_SUB_ADD = prove((parse_term @"!x y. (x - y) + y = x"), REAL_ARITH_TAC)
  let REAL_SUB_ADD2 = prove((parse_term @"!x y. y + (x - y) = x"), REAL_ARITH_TAC)
  let REAL_SUB_REFL = prove((parse_term @"!x. x - x = &0"), REAL_ARITH_TAC)
  let REAL_LE_DOUBLE = 
      prove((parse_term @"!x. &0 <= x + x <=> &0 <= x"), REAL_ARITH_TAC)
  let REAL_LE_NEGL = 
      prove((parse_term @"!x. (--x <= x) <=> (&0 <= x)"), REAL_ARITH_TAC)
  let REAL_LE_NEGR = 
      prove((parse_term @"!x. (x <= --x) <=> (x <= &0)"), REAL_ARITH_TAC)
  
  
negative.code: #endif
  
  let REAL_LE_RDIV_EQ = 
      prove((parse_term @"!x y z. &0 < z ==> (x <= y / z <=> x * z <= y)"), 
            REPEAT STRIP_TAC
            |> THEN <| FIRST_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [GSYM(MATCH_MP REAL_LE_RMUL_EQ th)])
            |> THEN <| ASM_SIMP_TAC [real_div;
                                     GSYM REAL_MUL_ASSOC;
                                     REAL_MUL_LINV;
                                     REAL_MUL_RID;
                                     REAL_LT_IMP_NZ])
  
  let REAL_LE_LDIV_EQ = 
      prove((parse_term @"!x y z. &0 < z ==> (x / z <= y <=> x <= y * z)"), 
            REPEAT STRIP_TAC
            |> THEN <| FIRST_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [GSYM(MATCH_MP REAL_LE_RMUL_EQ th)])
            |> THEN <| ASM_SIMP_TAC [real_div;
                                     GSYM REAL_MUL_ASSOC;
                                     REAL_MUL_LINV;
                                     REAL_MUL_RID;
                                     REAL_LT_IMP_NZ])
  
  let REAL_LT_RDIV_EQ = 
      prove
  