anchor.diff:                |> THEN <| CONV_TAC TAUT)
           match pth_geFuncs with
           | [pth_ge1; pth_ge2a; pth_ge2b; pth_ge3] -> pth_ge1, pth_ge2a, pth_ge2b, pth_ge3
  -        | _ -> failwith "pth_geFuncs: Unhandled case."
  +        | _ -> 
  +            let failThm = Choice.failwith "pth_geFuncs: Unhandled case."
  +            failThm, failThm, failThm, failThm
   
       let INT_GE_CONV = 
           FIRST_CONV [GEN_REWRITE_CONV I [pth_ge1]
  
positive.code: (* ------------------------------------------------------------------------- *)
  (* Hence define (positive) gcd function; add elimination to INTEGER_TAC.     *)
  (* ------------------------------------------------------------------------- *)
  do
      overload_interface("gcd", (parse_term @"int_gcd:int#int->int"))
      |> Choice.get
  
  let int_gcd = new_specification ["int_gcd"] (REWRITE_RULE[EXISTS_UNCURRY; SKOLEM_THM] INT_GCD_EXISTS_POS);;
  
  /// Automated tactic for elementary divisibility properties over the integers.
  let INTEGER_TAC =
    let GCD_ELIM_TAC =
      let gcd_tm = (parse_term @"gcd") in
      let dest_gcd tm =
        let l,r = Choice.get <| dest_comb tm in
        if l = gcd_tm then dest_pair r else failwith "dest_gcd" in
      REPEAT GEN_TAC |> THEN <|
      W(fun (asl,w) ->
            let gts =
              /// Tests for failure.
              let can f x = 
                  try f x |> ignore; true
                  with Failure _ -> false
              Choice.get <| find_terms (can dest_gcd) w in
            let ths = map (fun tm -> let a,b = Choice.get <| dest_gcd tm in SPECL [a;b] int_gcd) gts
            MAP_EVERY MP_TAC ths |> THEN <|
            MAP_EVERY SPEC_TAC (zip gts (map (genvar << Choice.get << type_of) gts))) in
    REPEAT(GEN_TAC |>ORELSE<| CONJ_TAC) |> THEN <| GCD_ELIM_TAC |> THEN <| INTEGER_TAC_001;;
  
  /// Automatically prove elementary divisibility property over the integers.
  let INTEGER_RULE tm = prove(tm,INTEGER_TAC);;a
  
  (* ------------------------------------------------------------------------- *)
  (* Mapping from nonnegative integers back to natural numbers.                *)
  
negative.code: (* Now define similar notions over the natural numbers.                      *)
  (* ------------------------------------------------------------------------- *)
  
  overload_interface("divides", (parse_term @"num_divides:num->num->bool")) |> ExtCore.Choice.bindOrRaise
  overload_interface("mod", (parse_term @"num_mod:num->num->num->bool")) |> ExtCore.Choice.bindOrRaise
  overload_interface("coprime", (parse_term @"num_coprime:num#num->bool")) |> ExtCore.Choice.bindOrRaise
  overload_interface("gcd", (parse_term @"num_gcd:num#num->num")) |> ExtCore.Choice.bindOrRaise
  
  let num_divides = new_definition(parse_term @"a divides b <=> &a divides &b")
  
  let num_mod = new_definition(parse_term @"(mod n) x y <=> (mod &n) (&x) (&y)")
  
  let num_congruent = 
      prove
          ((parse_term @"!x y n. (x == y) (mod n) <=> (&x == &y) (mod &n)"), 
           REWRITE_TAC [cong; num_mod])
  
  let num_coprime = new_definition(parse_term @"coprime(a,b) <=> coprime(&a,&b)")
  let num_gcd = new_definition(parse_term @"gcd(a,b) = num_of_int(gcd(&a,&b))")
  
  