anchor.diff:  (* ------------------------------------------------------------------------- *)
   (* Define operations on representatives of signed reals.                     *)
   (* ------------------------------------------------------------------------- *)
  +
   let treal_of_num = new_definition(parse_term @"treal_of_num n = (&n, &0)")
   
   let treal_neg = 
  
positive.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'
  
negative.code: 
  let DIST_LE_CASES, DIST_ADDBOUND, DIST_TRIANGLE, DIST_ADD2, DIST_ADD2_REV = 
      let rec DIST_ELIM_TAC = 
          let tac th gl =
              choice {
                  let! th = th
                  let! l, r = dest_eq(concl th)
                  if is_var l && not(vfree_in l r) then 
                      return! ALL_TAC gl
                  else 
                      return! ASSUME_TAC (Choice.result th) gl
              }
  
          let conv = HIGHER_REWRITE_CONV [SUB_ELIM_THM; COND_ELIM_THM; DIST_ELIM_THM] false
          CONV_TAC conv
          |> THEN <| TRY GEN_TAC
          |> THEN <| CONJ_TAC
          |> THEN <| DISCH_THEN(fun th -> 
                         SUBST_ALL_TAC th
                         |> THEN <| tac th)
  
      let DIST_ELIM_TAC' = 
          REPEAT STRIP_TAC
          |> THEN <| REPEAT DIST_ELIM_TAC
  