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:             real_le_antisym, real_le_trans, real_le_total, real_le_ladd_imp, 
              real_le_mul, real_inv_0, real_mul_linv, real_of_num_eq, real_of_num_le, 
              real_of_num_add, real_of_num_mul
      | _ -> failwith "realFuncs: Unhandled case."
  
  parse_as_prefix "--"
  parse_as_infix("/", (22, "left"))
  
negative.code: 
      match distFuncs with
      | [dist_triangle; dist_add2; dist_add2_rev] -> DIST_LE_CASES, DIST_ADDBOUND, dist_triangle, dist_add2, dist_add2_rev
      | _ -> 
          Choice.failwith "distFuncs: Unhandled case.",
          Choice.failwith "distFuncs: Unhandled case.",
          Choice.failwith "distFuncs: Unhandled case.",
          Choice.failwith "distFuncs: Unhandled case.",
          Choice.failwith "distFuncs: Unhandled case."
  
  let DIST_TRIANGLE_LE = 
      prove
  