anchor.diff:            hreal_le_add, hreal_le_exists, hreal_arch, hreal_add_sym, hreal_add_assoc, 
             hreal_add_lid, hreal_add_lcancel, hreal_mul_sym, hreal_mul_assoc, 
             hreal_mul_lid, hreal_add_ldistrib, hreal_mul_linv, hreal_inv_0
  -    | _ -> failwith "naddFuncs: Unhandled case."
  +    | _ -> 
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case.",
  +        Choice.failwith "naddFuncs: Unhandled case."
   
   (* ------------------------------------------------------------------------- *)
   (* Consequential theorems needed later.                                      *)
   (* ------------------------------------------------------------------------- *)
  +
   let HREAL_LE_EXISTS_DEF = 
       prove
           ((parse_term @"!m n. m <= n <=> ?d. n = m + d"), 
  
positive.code: 
      match distFuncs with
      | [dist_triangle; dist_add2; dist_add2_rev] -> DIST_LE_CASES, DIST_ADDBOUND, dist_triangle, dist_add2, dist_add2_rev
      | _ -> failwith "distFuncs: Unhnadled case."
  
  let DIST_TRIANGLE_LE = 
      prove
  
negative.code:          |> THEN <| ASM_REWRITE_TAC [])
  
  let NADD_MUL_WELLDEF_LEMMA = 
      prove((parse_term @"!x y y'. y === y' ==> (x ** y) === (x ** y')"), 
            REPEAT GEN_TAC
            |> THEN <| REWRITE_TAC [nadd_eq; NADD_MUL]
            |> THEN <| DISCH_THEN(X_CHOOSE_TAC(parse_term @"B1:num"))
            |> THEN <| X_CHOOSE_TAC (parse_term @"B2:num") (SPEC (parse_term @"x:nadd") NADD_DIST)
            |> THEN <| EXISTS_TAC(parse_term @"B2 * B1")
            |> THEN <| X_GEN_TAC(parse_term @"n:num")
            |> THEN <| MATCH_MP_TAC LE_TRANS
            |> THEN <| EXISTS_TAC(parse_term @"B2 * dist(fn y n,fn y' n)")
            |> THEN <| ASM_REWRITE_TAC [LE_MULT_LCANCEL])
  
  let NADD_MUL_WELLDEF = 
      prove((parse_term @"!x x' y y'. x === x' /\ y === y'
  