anchor.diff:           |> THEN <| ASM_REWRITE_TAC [LE; ADD_CLAUSES; LE_REFL])
   
   let LE_ADDR = 
  -    prove((parse_term @"!m n. n <= m + n"), ONCE_REWRITE_TAC [ADD_SYM]
  -                                           |> THEN <| MATCH_ACCEPT_TAC LE_ADD)
  +    prove((parse_term @"!m n. n <= m + n"), 
  +          ONCE_REWRITE_TAC [ADD_SYM]
  +          |> THEN <| MATCH_ACCEPT_TAC LE_ADD)
  +
   let LT_ADD = 
       prove
           ((parse_term @"!m n. (m < m + n) <=> (0 < n)"), 
            INDUCT_TAC
            |> THEN <| ASM_REWRITE_TAC [ADD_CLAUSES; LT_SUC])
  +
   let LT_ADDR = 
       prove
           ((parse_term @"!m n. (n < m + n) <=> (0 < m)"), 
  
positive.code:                       |> THEN <| ASM_REWRITE_TAC []])
  
  let NOT_LE = 
      prove
          ((parse_term @"!m n. ~(m <= n) <=> (n < m)"), 
           REPEAT INDUCT_TAC
           |> THEN <| ASM_REWRITE_TAC [LE_SUC; LT_SUC]
           |> THEN <| REWRITE_TAC [LE
                                   LT
                                   NOT_SUC
                                   GSYM NOT_SUC
                                   LE_0]
           |> THEN <| W(W(curry SPEC_TAC) << hd << frees << snd)
           |> THEN <| INDUCT_TAC
           |> THEN <| REWRITE_TAC [LT_0])
  
  let NOT_LT = 
      prove
          ((parse_term @"!m n. ~(m < n) <=> n <= m"), REPEAT INDUCT_TAC
                                                     |> THEN 
                                                     <| ASM_REWRITE_TAC 
                                                            [LE_SUC; LT_SUC]
                                                     |> THEN <| REWRITE_TAC [LE
                                                                             LT
                                                                             NOT_SUC
                                                                             GSYM 
                                                                                 NOT_SUC
                                                                             LE_0]
                                                     |> THEN 
                                                     <| W
                                                            (W(curry SPEC_TAC) 
                                                             << hd << frees << snd)
                                                     |> THEN <| INDUCT_TAC
                                                     |> THEN <| REWRITE_TAC [LT_0])
  
  let LT_IMP_LE = 
      prove((parse_term @"!m n. m < n ==> m <= n"), REWRITE_TAC [LT_LE]
                                                   |> THEN <| REPEAT STRIP_TAC
                                                   |> THEN <| ASM_REWRITE_TAC [])
  
  let EQ_IMP_LE = 
      prove
  
negative.code: (* ------------------------------------------------------------------------- *)
  (* Exponentiation.                                                           *)
  (* ------------------------------------------------------------------------- *)
  
  let EXP = 
      new_recursive_definition num_RECURSION (parse_term @"(!m. m EXP 0 = 1) /\
     (!m n. m EXP (SUC n) = m * (m EXP n))")
  
  let EXP_EQ_0 = 
  