anchor.diff:           |> THEN <| ASM_MESON_TAC [LE_ADD; LE])
   
   let DIV_LE_EXCLUSION = 
  -    prove
  -        ((parse_term @"!a b c d. ~(b = 0) /\ b * c < (a + 1) * d ==> c DIV d <= a DIV b"), 
  -         REPEAT GEN_TAC
  -         |> THEN <| ASM_CASES_TAC(parse_term @"d = 0")
  -         |> THEN <| ASM_REWRITE_TAC [MULT_CLAUSES; LT]
  -         |> THEN <| STRIP_TAC
  -         |> THEN 
  -         <| MATCH_MP_TAC
  -                (MESON [LE_REFL] 
  -                     (parse_term @"(!k:num. k <= a ==> k <= b) ==> a <= b"))
  -         |> THEN <| X_GEN_TAC(parse_term @"k:num")
  -         |> THEN 
  -         <| SUBGOAL_THEN 
  -                (parse_term @"b * d * k <= b * c ==> (b * k) * d < (a + 1) * d") 
  -                MP_TAC
  -         |> THENL <| [ASM_MESON_TAC [LET_TRANS; MULT_AC]
  -                      ALL_TAC]
  -         |> THEN <| MATCH_MP_TAC MONO_IMP
  -         |> THEN <| ASM_SIMP_TAC [LE_MULT_LCANCEL; LT_MULT_RCANCEL; LE_RDIV_EQ]
  -         |> THEN <| REWRITE_TAC [GSYM ADD1
  -                                 LT_SUC_LE])
  +    prove((parse_term @"!a b c d. ~(b = 0) /\ b * c < (a + 1) * d ==> c DIV d <= a DIV b"), 
  +          REPEAT GEN_TAC
  +          |> THEN <| ASM_CASES_TAC(parse_term @"d = 0")
  +          |> THEN <| ASM_REWRITE_TAC [MULT_CLAUSES; LT]
  +          |> THEN <| STRIP_TAC
  +          |> THEN <| MATCH_MP_TAC(MESON [LE_REFL] (parse_term @"(!k:num. k <= a ==> k <= b) ==> a <= b"))
  +          |> THEN <| X_GEN_TAC(parse_term @"k:num")
  +          |> THEN <| SUBGOAL_THEN (parse_term @"b * d * k <= b * c ==> (b * k) * d < (a + 1) * d") MP_TAC
  +          |> THENL <| [ASM_MESON_TAC [LET_TRANS; MULT_AC];
  +                       ALL_TAC]
  +          |> THEN <| MATCH_MP_TAC MONO_IMP
  +          |> THEN <| ASM_SIMP_TAC [LE_MULT_LCANCEL; LT_MULT_RCANCEL; LE_RDIV_EQ]
  +          |> THEN <| REWRITE_TAC [GSYM ADD1;
  +                                  LT_SUC_LE])
   
   let DIV_EQ_EXCLUSION = 
       prove
  
positive.code:          |> THEN <| REWRITE_TAC [TWO; NOT_SUC])
  
  let ODD_MOD = 
      prove
          ((parse_term @"!n. ODD(n) <=> (n MOD 2 = 1)"), 
           GEN_TAC
           |> THEN <| REWRITE_TAC [GSYM NOT_EVEN
                                   EVEN_MOD]
           |> THEN <| SUBGOAL_THEN (parse_term @"n MOD 2 < 2") MP_TAC
           |> THENL <| [SIMP_TAC [DIVISION; TWO; NOT_SUC]
                        ALL_TAC]
           |> THEN <| SPEC_TAC((parse_term @"n MOD 2"), (parse_term @"n:num"))
           |> THEN <| REWRITE_TAC [TWO; ONE; LT]
           |> THEN <| MESON_TAC [NOT_SUC])
  
  let MOD_MULT_RMOD = 
      prove
          ((parse_term @"!m n p. ~(n = 0) ==> ((m * (p MOD n)) MOD n = (m * p) MOD n)"), 
           REPEAT STRIP_TAC
           |> THEN <| CONV_TAC SYM_CONV
           |> THEN <| MATCH_MP_TAC MOD_EQ
           |> THEN <| EXISTS_TAC(parse_term @"m * p DIV n")
           |> THEN <| REWRITE_TAC [GSYM MULT_ASSOC
                                   GSYM LEFT_ADD_DISTRIB]
           |> THEN <| REWRITE_TAC [EQ_MULT_LCANCEL]
           |> THEN <| DISJ2_TAC
           |> THEN <| ONCE_REWRITE_TAC [ADD_SYM]
           |> THEN <| ASM_SIMP_TAC [DIVISION])
  
  let MOD_MULT_LMOD = 
      prove
          ((parse_term @"!m n p. ~(n = 0) ==> (((m MOD n) * p) MOD n = (m * p) MOD n)"), 
           ONCE_REWRITE_TAC [MULT_SYM]
           |> THEN <| SIMP_TAC [MOD_MULT_RMOD])
  let MOD_MULT_MOD2 = 
      prove
          ((parse_term @"!m n p. ~(n = 0) ==> (((m MOD n) * (p MOD n)) MOD n = (m * p) MOD n)"), 
           SIMP_TAC [MOD_MULT_RMOD; MOD_MULT_LMOD])
  
  let MOD_EXP_MOD = 
      prove
          ((parse_term @"!m n p. ~(n = 0) ==> (((m MOD n) EXP p) MOD n = (m EXP p) MOD n)"), 
           REPEAT STRIP_TAC
           |> THEN <| SPEC_TAC((parse_term @"p:num"), (parse_term @"p:num"))
           |> THEN <| INDUCT_TAC
           |> THEN <| ASM_REWRITE_TAC [EXP]
           |> THEN <| ASM_SIMP_TAC [MOD_MULT_LMOD]
           |> THEN <| MATCH_MP_TAC EQ_TRANS
           |> THEN <| EXISTS_TAC(parse_term @"(m * ((m MOD n) EXP p) MOD n) MOD n")
           |> THEN <| CONJ_TAC
           |> THENL <| [ALL_TAC
                        ASM_REWRITE_TAC []]
           |> THEN <| ASM_SIMP_TAC [MOD_MULT_RMOD])
  
  let MOD_MULT_ADD = 
      prove
          ((parse_term @"!m n p. (m * n + p) MOD n = p MOD n"), 
           REPEAT STRIP_TAC
           |> THEN <| ASM_CASES_TAC(parse_term @"n = 0")
           |> THEN <| ASM_REWRITE_TAC [MULT_CLAUSES; ADD_CLAUSES]
           |> THEN <| MATCH_MP_TAC MOD_UNIQ
           |> THEN <| EXISTS_TAC(parse_term @"m + p DIV n")
           |> THEN <| ASM_SIMP_TAC [RIGHT_ADD_DISTRIB
                                    GSYM ADD_ASSOC
                                    EQ_ADD_LCANCEL; DIVISION])
  
  let DIV_MULT_ADD = 
      prove
          ((parse_term @"!a b n. ~(n = 0) ==> (a * n + b) DIV n = a + b DIV n"), 
           REPEAT STRIP_TAC
           |> THEN <| MATCH_MP_TAC DIV_UNIQ
           |> THEN <| EXISTS_TAC(parse_term @"b MOD n")
           |> THEN <| REWRITE_TAC [RIGHT_ADD_DISTRIB
                                   GSYM ADD_ASSOC]
           |> THEN <| ASM_MESON_TAC [DIVISION])
  
  let MOD_ADD_MOD = 
      prove
          ((parse_term @"!a b n. ~(n = 0) ==> ((a MOD n + b MOD n) MOD n = (a + b) MOD n)"), 
           REPEAT STRIP_TAC
           |> THEN <| CONV_TAC SYM_CONV
           |> THEN <| MATCH_MP_TAC MOD_EQ
           |> THEN <| EXISTS_TAC(parse_term @"a DIV n + b DIV n")
           |> THEN <| REWRITE_TAC [RIGHT_ADD_DISTRIB]
           |> THEN 
           <| ONCE_REWRITE_TAC 
                  [AC ADD_AC (parse_term @"(a + b) + (c + d) = (c + a) + (d + b)")]
           |> THEN <| BINOP_TAC
           |> THEN <| ASM_SIMP_TAC [DIVISION])
  
  let DIV_ADD_MOD = 
      prove((parse_term @"!a b n. ~(n = 0)
              ==> (((a + b) MOD n = a MOD n + b MOD n) <=>
                   ((a + b) DIV n = a DIV n + b DIV n))"),
       REPEAT STRIP_TAC
                  |> THEN <| FIRST_ASSUM(MP_TAC << MATCH_MP DIVISION)
                  |> THEN 
                  <| DISCH_THEN
                         (fun th -> 
                             MAP_EVERY (MP_TAC << CONJUNCT1 << C SPEC th) 
                                 [(parse_term @"a + b:num")
                                  (parse_term @"a:num")
                                  (parse_term @"b:num")])
                  |> THEN 
                  <| DISCH_THEN
                         (fun th1 -> 
                             DISCH_THEN
                                 (fun th2 -> 
                                     MP_TAC
                                         (MK_COMB
                                              (AP_TERM (parse_term @"(+)") th2, th1))))
                  |> THEN 
                  <| DISCH_THEN
                         (fun th -> GEN_REWRITE_TAC (funpow 2 LAND_CONV) [th])
                  |> THEN 
                  <| ONCE_REWRITE_TAC 
                         [AC ADD_AC 
                              (parse_term @"(a + b) + c + d = (a + c) + (b + d)")]
                  |> THEN <| REWRITE_TAC [GSYM RIGHT_ADD_DISTRIB]
                  |> THEN <| DISCH_THEN(fun th -> 
                                     EQ_TAC
                                     |> THEN <| DISCH_TAC
                                     |> THEN <| MP_TAC th)
                  |> THEN 
                  <| ASM_REWRITE_TAC 
                         [EQ_ADD_RCANCEL; EQ_ADD_LCANCEL; EQ_MULT_RCANCEL]
                  |> THEN <| REWRITE_TAC [EQ_SYM_EQ])
  
  let DIV_REFL = 
      prove
  
negative.code:     prove((parse_term @"!R. (!x. R x x) /\ (!x y z. R x y /\ R y z ==> R x z) /\
          (!n. R n (SUC n))
          ==> !m n. m <= n ==> R m n"),
            REPEAT GEN_TAC
            |> THEN <| MATCH_MP_TAC(TAUT(parse_term @"(a /\ a' ==> (c <=> b)) ==> a /\ a' /\ b ==> c"))
            |> THEN <| MATCH_ACCEPT_TAC TRANSITIVE_STEPWISE_LE_EQ)
  