anchor.diff:           |> THEN <| REAL_ARITH_TAC)
   
   let REAL_SGN = 
  -    prove
  -        ((parse_term @"!x. real_sgn x = x / abs x"), 
  -         GEN_TAC
  -         |> THEN <| ASM_CASES_TAC(parse_term @"x = &0")
  -         |> THENL 
  -         <| [ASM_REWRITE_TAC [real_div; REAL_MUL_LZERO; REAL_SGN_0]
  -             GEN_REWRITE_TAC (RAND_CONV << LAND_CONV) [GSYM REAL_SGN_ABS]
  -             |> THEN 
  -             <| ASM_SIMP_TAC [real_div
  -                              GSYM REAL_MUL_ASSOC
  -                              REAL_ABS_ZERO; REAL_MUL_RINV; REAL_MUL_RID]])
  +    prove((parse_term @"!x. real_sgn x = x / abs x"), 
  +          GEN_TAC
  +          |> THEN <| ASM_CASES_TAC(parse_term @"x = &0")
  +          |> THENL <| [ASM_REWRITE_TAC [real_div; REAL_MUL_LZERO; REAL_SGN_0];
  +                       GEN_REWRITE_TAC (RAND_CONV << LAND_CONV) [GSYM REAL_SGN_ABS]
  +                       |> THEN <| ASM_SIMP_TAC [real_div;
  +                                                GSYM REAL_MUL_ASSOC;
  +                                                REAL_ABS_ZERO;
  +                                                REAL_MUL_RINV;
  +                                                REAL_MUL_RID]])
   
   let REAL_SGN_MUL = 
       prove
  
positive.code: #endif
  
  let REAL_ABS_0 = prove((parse_term @"abs(&0) = &0"), REAL_ARITH_TAC)
  let REAL_ABS_1 = prove((parse_term @"abs(&1) = &1"), REAL_ARITH_TAC)
  let REAL_ABS_TRIANGLE = 
      prove((parse_term @"!x y. abs(x + y) <= abs(x) + abs(y)"), REAL_ARITH_TAC)
  let REAL_ABS_TRIANGLE_LE = 
      prove
          ((parse_term @"!x y z.abs(x) + abs(y - x) <= z ==> abs(y) <= z"), 
           REAL_ARITH_TAC)
  let REAL_ABS_TRIANGLE_LT = 
      prove
          ((parse_term @"!x y z.abs(x) + abs(y - x) < z ==> abs(y) < z"), 
           REAL_ARITH_TAC)
  let REAL_ABS_POS = prove((parse_term @"!x. &0 <= abs(x)"), REAL_ARITH_TAC)
  let REAL_ABS_SUB = 
      prove((parse_term @"!x y. abs(x - y) = abs(y - x)"), REAL_ARITH_TAC)
  
  
negative.code: 
  let REAL_SOS_EQ_0 = 
  #if BUGGY
      prove((parse_term @"!x y. x pow 2 + y pow 2 = &0 <=> x = &0 /\ y = &0"), 
            REPEAT GEN_TAC
            |> THEN <| EQ_TAC
            |> THEN <| SIMP_TAC [REAL_POW_2; REAL_MUL_LZERO; REAL_ADD_LID]
            |> THEN <| DISCH_THEN
                          (MP_TAC << MATCH_MP(REAL_ARITH(parse_term @"x + y = &0 ==> &0 <= x /\ &0 <= y ==> x = &0 /\ y = &0")))
            |> THEN <| REWRITE_TAC [REAL_LE_SQUARE; REAL_ENTIRE])
  #else
      Choice.result <| Sequent([],parse_term @"!x y. x pow 2 + y pow 2 = &0 <=> x = &0 /\ y = &0") : thm
  #endif
  