anchor.diff:  (* ------------------------------------------------------------------------- *)
   (* Set up overloading so we can use same symbols for N, Z and even R.        *)
   (* ------------------------------------------------------------------------- *)
  +
  +make_overloadable "divides" (parse_type ":A->A->bool");;
  +make_overloadable "mod" (parse_type ":A->A->A->bool");;
  +make_overloadable "coprime" (parse_type ":A#A->bool");;
  +make_overloadable "gcd" (parse_type ":A#A->A");;
  +
   (* ------------------------------------------------------------------------- *)
   (* The general notion of congruence: just syntax for equivalence relation.   *)
   (* ------------------------------------------------------------------------- *)
  +parse_as_infix("==",(10,"right"));;
  +
   let cong = new_definition(parse_term "(x == y) (rel:A->A->bool) <=> rel x y")
   
   (* ------------------------------------------------------------------------- *)
  
positive.code:          |> THEN <| POP_ASSUM(MP_TAC << AP_TERM(parse_term "int_of_real"))
           |> THEN <| REWRITE_TAC [int_abstr])
  
  do_list overload_interface ["+", (parse_term "int_add:int->int->int")
                              "-", (parse_term "int_sub:int->int->int")
                              "*", (parse_term "int_mul:int->int->int")
  
negative.code:                       GSYM FORALL_PAIR_THM;
                        WF_INT_MEASURE])
  
  let INT_GCD_EXISTS = 
   prove ((parse_term "!a b. ?d. d divides a /\ d divides b /\ ?x y. d = a * x + b * y"),
    let INT_GCD_EXISTS_CASES = 
     INT_ARITH (parse_term "(a = &0 \/ b = &0) \/
      abs(a - b) + abs b < abs a + abs b \/ abs(a + b) + abs b < abs a + abs b \/
      abs a + abs(b - a) < abs a + abs b \/ abs a + abs(b + a) < abs a + abs b") in
    MATCH_MP_TAC WF_INT_MEASURE_2 |>THEN<| EXISTS_TAC (parse_term "\x y. abs(x) + abs(y)") |>THEN<|
    REWRITE_TAC[] |>THEN<| REPEAT STRIP_TAC |>THENL<| [INT_ARITH_TAC; ALL_TAC] |>THEN<|
    DISJ_CASES_THEN MP_TAC INT_GCD_EXISTS_CASES |>THENL<|
     [STRIP_TAC |>THEN<| ASM_REWRITE_TAC[INTEGER_RULE_001 (parse_term "d divides &0")] |>THEN<|
      REWRITE_TAC[INT_MUL_LZERO; INT_ADD_LID; INT_ADD_RID] |>THEN<|
      MESON_TAC[INTEGER_RULE_001 (parse_term "d divides d"); INT_MUL_RID];
      DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN (ANTE_RES_THEN MP_TAC)) |>THEN<|
      MATCH_MP_TAC MONO_EXISTS |>THEN<| INTEGER_TAC_001]);;
  
  let INT_GCD_EXISTS_POS = 
   prove ((parse_term "!a b. ?d. &0 <= d /\ d divides a /\ d divides b /\ ?x y. d = a * x + b * y"),
    REPEAT GEN_TAC |>THEN<|
    X_CHOOSE_TAC (parse_term "d:int") (SPECL [(parse_term "a:int"); (parse_term "b:int")] INT_GCD_EXISTS) |>THEN<|
    DISJ_CASES_TAC(SPEC (parse_term "d:int") INT_LE_NEGTOTAL) |>THEN<|
    ASM_MESON_TAC[INTEGER_RULE_001 (parse_term "(--d) divides x <=> d divides x");
                  INT_ARITH (parse_term "a * --x + b * --y = --(a * x + b * y)")]);;
  
  (* ------------------------------------------------------------------------- *)
  (* Hence define (positive) gcd function; add elimination to INTEGER_TAC.     *)
  (* ------------------------------------------------------------------------- *)
  overload_interface("gcd", (parse_term "int_gcd:int#int->int"))
  
  let int_gcd = new_specification ["int_gcd"] (REWRITE_RULE[EXISTS_UNCURRY; SKOLEM_THM] INT_GCD_EXISTS_POS);;
  
  let INTEGER_TAC =
    let GCD_ELIM_TAC =
      let gcd_tm = (parse_term "gcd") in
      let dest_gcd tm =
        let l,r = 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 = find_terms (can dest_gcd) w in
            let ths = map (fun tm -> let a,b = dest_gcd tm in SPECL [a;b] int_gcd) gts
            MAP_EVERY MP_TAC ths |>THEN<|
            MAP_EVERY SPEC_TAC (zip gts (map (genvar << type_of) gts))) in
    REPEAT(GEN_TAC |>ORELSE<| CONJ_TAC) |>THEN<| GCD_ELIM_TAC |>THEN<| INTEGER_TAC_001;;
  
  let INTEGER_RULE tm = prove(tm,INTEGER_TAC);;
  
  
  (* ------------------------------------------------------------------------- *)
  (* Mapping from nonnegative integers back to natural numbers.                *)
  (* ------------------------------------------------------------------------- *)
  