anchor.diff:      let int_ty = (parse_type @"int")
       let INT_POLYEQ_CONV = GEN_REWRITE_CONV I [GSYM INT_SUB_0]
                             |> THENC <| LAND_CONV INT_POLY_CONV
  +
       let ISOLATE_VARIABLE = 
           // CAUTION: change from value to function to delay System.Exception
           let pth() = INT_ARITH(parse_term @"!a x. a = &0 <=> x = x + a")
  
positive.code:         let mul_tm = (parse_term @"(int_mul)")
          let add_tm = (parse_term @"(int_add)")
          let neg_tm = (parse_term @"(int_neg)")
          let dest_mul = Choice.get << dest_binop mul_tm
          let dest_add = Choice.get << dest_binop add_tm
          let mk_mul = fun x -> Choice.get << mk_binop mul_tm x
          let mk_add = fun x -> Choice.get << mk_binop add_tm x
          let scrub_var v m = 
              let ps = striplist (Some << dest_mul) m
              let ps' = subtract ps [v]
              if ps' = []
              then one_tm
              else end_itlist mk_mul ps'
          let find_multipliers v mons = 
              let mons1 = filter (fun m -> free_in v m) mons
              let mons2 = map (scrub_var v) mons1
              if mons2 = []
              then zero_tm
              else end_itlist mk_add mons2
          fun vars tm -> 
              let cmons, vmons = 
                  partition (fun m -> intersect (frees m) vars = []) 
                      (striplist (Some << dest_add) tm)
              let cofactors = map (fun v -> find_multipliers v vmons) vars
              let cnc = 
                  if cmons = []
                  then zero_tm
                  else Choice.get <| mk_comb(neg_tm, end_itlist mk_add cmons)
              cofactors, cnc
      let isolate_variables evs ps eq = 
          let vars = filter (fun v -> vfree_in v eq) evs
          let qs, p = isolate_monomials vars eq
          let rs = filter (fun t -> Choice.get <| type_of t = int_ty) (qs @ ps)
          let rs = int_ideal_cofactors rs p
          eq, zip (fst(chop_list (length qs) rs)) vars
  
      let subst_in_poly i p = Choice.get <| rhs(concl <| Choice.get(INT_POLY_CONV(Choice.get <| vsubst i p)))
      let rec solve_idealism evs ps eqs = 
          if evs = []
          then []
          else 
              let eq, cfs = 
                  tryfind (Some << isolate_variables evs ps) eqs
                  |> Option.getOrFailWith "tryfind"
                      
              let evs' = subtract evs (map snd cfs)
              let eqs' = map (subst_in_poly cfs) (subtract eqs [eq])
              cfs @ solve_idealism evs' ps eqs'
      let rec GENVAR_EXISTS_CONV tm = 
          if not(is_exists tm)
          then REFL tm
          else 
              let ev, bod = Choice.get <| dest_exists tm
              let gv = genvar(Choice.get <| type_of ev)
              (GEN_ALPHA_CONV gv
               |> THENC <| BINDER_CONV GENVAR_EXISTS_CONV) tm
      let EXISTS_POLY_TAC(asl, w as gl) = 
          let evs, bod = strip_exists w
          let ps = 
              mapfilter 
                  (Choice.toOption << check(fun t -> Choice.get <| type_of t = int_ty) << Choice.get << lhs << concl << Choice.get << snd) asl
          let cfs = solve_idealism evs ps (map (Choice.get << lhs) (conjuncts bod))
          (MAP_EVERY EXISTS_TAC (map (fun v -> rev_assocd v cfs zero_tm) evs)
           |> THEN <| REPEAT(POP_ASSUM MP_TAC)
           |> THEN <| CONV_TAC INT_RING) gl
  
      let SCRUB_NEQ_TAC = 
          MATCH_MP_TAC 
  
negative.code:             let! r' = dest_intconst r
              return! CONJUNCT2(INT_DIVMOD_CONV l' r')
          }
          |> Choice.mapError (fun e -> nestedFailure e "INT_MOD_CONV"));;
  
  /// Performs one arithmetic or relational operation on integer literals of type :int.
  let INT_RED_CONV = 
  