anchor.diff:                    |> THEN <| REWRITE_TAC [INT_ADD_RINV; INT_ADD_LID])
           match pthFuncs with
           | [pth1; pth2; pth3; pth4; pth5; pth6] -> pth1, pth2, pth3, pth4, pth5, pth6
  -        | _ -> failwith "pthFuncs: Unhandled case."
  +        | _ ->
  +            let failThm = Choice.failwith "pthFuncs: Unhandled case."
  +            failThm, failThm, failThm, failThm, failThm, failThm
   
       GEN_REWRITE_CONV I [pth0]
       |> ORELSEC <| (fun tm -> 
  
positive.code:     new_definition
          (parse_term @"real_mod n (x:real) y = ?q. integer q /\ x - y = q * n")
  
  overload_interface("mod", (parse_term @"real_mod")) |> ignore;;
  
  (* ------------------------------------------------------------------------- *)
  (* Integer divisibility.                                                     *)
  (* ------------------------------------------------------------------------- *)
  
  parse_as_infix("divides", (12, "right"))
  overload_interface("divides", (parse_term @"int_divides:int->int->bool")) |> ignore
  
  let int_divides = new_definition(parse_term @"a divides b <=> ?x. b = a * x")
  
  
negative.code: (* ------------------------------------------------------------------------- *)
  (* Hence define (positive) gcd function; add elimination to INTEGER_TAC.     *)
  (* ------------------------------------------------------------------------- *)
  
  overload_interface("gcd", (parse_term @"int_gcd:int#int->int")) |> ExtCore.Choice.bindOrRaise
  
  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")
          let dest_gcd tm = 
              choice {
                  let! l, r = dest_comb tm
                  if l = gcd_tm then 
                      return! dest_pair r
                  else 
                      return! Choice.failwith "dest_gcd"
              }
  
          REPEAT GEN_TAC
          |> THEN <| W(fun (asl, w) -> 
                         // NOTE: add arguments to propagate errors
                         fun gl ->
                          choice {
                             let! gts = find_terms (Choice.isResult << dest_gcd) w
                             let! ths = 
                                 Choice.List.map (fun tm -> 
                                     choice {
                                         let! a, b = dest_gcd tm
                                         return SPECL [a; b] int_gcd
                                     }) gts
                             return!
                                 (MAP_EVERY MP_TAC ths
                                  |> THEN <| MAP_EVERY SPEC_TAC (zip gts (map (genvar << Choice.get << type_of) gts))) gl
                          })
      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);;
  
  (* ------------------------------------------------------------------------- *)
  (* Mapping from nonnegative integers back to natural numbers.                *)
  