anchor.diff:  
   let REAL_LT_INV = 
   #if BUGGY
  -    prove
  -        ((parse_term @"!x. &0 < x ==> &0 < inv(x)"), 
  -         GEN_TAC
  -         |> THEN 
  -         <| REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC 
  -                (SPEC (parse_term @"inv(x)") REAL_LT_NEGTOTAL)
  -         |> THEN <| ASM_REWRITE_TAC []
  -         |> THENL <| [RULE_ASSUM_TAC(REWRITE_RULE [REAL_INV_EQ_0])
  -                      |> THEN <| ASM_REWRITE_TAC []
  -                      DISCH_TAC
  -                      |> THEN 
  -                      <| SUBGOAL_THEN (parse_term @"&0 < --(inv x) * x") MP_TAC
  -                      |> THENL <| [MATCH_MP_TAC REAL_LT_MUL
  -                                   |> THEN <| ASM_REWRITE_TAC []
  -                                   REWRITE_TAC [REAL_MUL_LNEG]]]
  -         |> THEN <| SUBGOAL_THEN (parse_term @"inv(x) * x = &1") SUBST1_TAC
  -         |> THENL 
  -         <| [MATCH_MP_TAC REAL_MUL_LINV
  -             |> THEN <| UNDISCH_TAC(parse_term @"&0 < x")
  -             |> THEN <| REAL_ARITH_TAC
  -             REWRITE_TAC [REAL_LT_RNEG; REAL_ADD_LID; REAL_OF_NUM_LT; ARITH]])
  +    prove((parse_term @"!x. &0 < x ==> &0 < inv(x)"), 
  +          GEN_TAC
  +          |> THEN <| REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPEC (parse_term @"inv(x)") REAL_LT_NEGTOTAL)
  +          |> THEN <| ASM_REWRITE_TAC []
  +          |> THENL <| [RULE_ASSUM_TAC(REWRITE_RULE [REAL_INV_EQ_0])
  +                       |> THEN <| ASM_REWRITE_TAC [];
  +                       DISCH_TAC
  +                       |> THEN <| SUBGOAL_THEN (parse_term @"&0 < --(inv x) * x") MP_TAC
  +                       |> THENL <| [MATCH_MP_TAC REAL_LT_MUL
  +                                    |> THEN <| ASM_REWRITE_TAC [];
  +                                    REWRITE_TAC [REAL_MUL_LNEG]]]
  +          |> THEN <| SUBGOAL_THEN (parse_term @"inv(x) * x = &1") SUBST1_TAC
  +          |> THENL <| [MATCH_MP_TAC REAL_MUL_LINV
  +                       |> THEN <| UNDISCH_TAC(parse_term @"&0 < x")
  +                       |> THEN <| REAL_ARITH_TAC;
  +                       REWRITE_TAC [REAL_LT_RNEG; REAL_ADD_LID; REAL_OF_NUM_LT; ARITH]])
   #else
       Choice.result <| Sequent([],parse_term @"!x. &0 < x ==> &0 < inv(x)") : thm
   #endif
  
positive.code: (* ------------------------------------------------------------------------- *)
  (* Tactic version of REAL_ARITH.                                             *)
  (* ------------------------------------------------------------------------- *)
  /// Attempt to prove goal using basic algebra and linear arithmetic over the reals.
  let REAL_ARITH_TAC = CONV_TAC REAL_ARITH
  
  (* ------------------------------------------------------------------------- *)
  (* Prove all the linear theorems we can blow away automatically.             *)
  (* ------------------------------------------------------------------------- *)
  let REAL_EQ_ADD_LCANCEL_0 = 
  #if BUGGY
      prove((parse_term @"!x y. (x + y = x) <=> (y = &0)"), REAL_ARITH_TAC)
  
negative.code:     prove
          ((parse_term @"!x n. inv(x pow n) = (inv x) pow n"), 
           REWRITE_TAC [REAL_POW_INV])
  
  let REAL_POW_DIV = 
      prove
          ((parse_term @"!x y n. (x / y) pow n = (x pow n) / (y pow n)"), 
           REWRITE_TAC [real_div; REAL_POW_MUL; REAL_POW_INV])
  
  let REAL_DIV_EQ_0 = 
      prove
          ((parse_term @"!x y. x / y = &0 <=> x = &0 \/ y = &0"), 
           REWRITE_TAC [real_div; REAL_INV_EQ_0; REAL_ENTIRE])
  
  let REAL_POW_ADD = 
      prove((parse_term @"!x m n. x pow (m + n) = x pow m * x pow n"), 
            GEN_TAC
            |> THEN <| INDUCT_TAC
            |> THEN <| ASM_REWRITE_TAC [ADD_CLAUSES; real_pow; REAL_MUL_LID; REAL_MUL_ASSOC])
  
  let REAL_POW_NZ = 
      prove
  