anchor.diff:  let TRANSITIVE_STEPWISE_LT = 
       prove((parse_term @"!R. (!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 ==> (c <=> b)) ==> a /\ b ==> c"))
  -       |> THEN <| MATCH_ACCEPT_TAC TRANSITIVE_STEPWISE_LT_EQ)
  +          REPEAT GEN_TAC
  +          |> THEN <| MATCH_MP_TAC(TAUT(parse_term @"(a ==> (c <=> b)) ==> a /\ b ==> c"))
  +          |> THEN <| MATCH_ACCEPT_TAC TRANSITIVE_STEPWISE_LT_EQ)
   
   let TRANSITIVE_STEPWISE_LE_EQ = 
       prove((parse_term @"!R. (!x. R x x) /\ (!x y z. R x y /\ R y z ==> R x z)
  
positive.code:          |> THEN <| MESON_TAC [])
  
  let PRE_ELIM_THM' = 
      prove
          ((parse_term @"P(PRE n) <=> ?m. (n = SUC m \/ m = 0 /\ n = 0) /\ P m"), 
           MP_TAC
               (INST [(parse_term @"\x:num. ~P x"), (parse_term @"P:num->bool")] 
                    PRE_ELIM_THM)
           |> THEN <| MESON_TAC [])
  
  let SUB_ELIM_THM = 
      prove
          ((parse_term @"P(a - b) <=> !d. a = b + d \/ a < b /\ d = 0 ==> P d"), 
           DISJ_CASES_TAC(SPECL [(parse_term @"a:num")
                                 (parse_term @"b:num")] LTE_CASES)
           |> THENL <| [ASM_MESON_TAC [NOT_LT; SUB_EQ_0; LT_IMP_LE; LE_ADD]
                        ALL_TAC]
           |> THEN 
           <| FIRST_ASSUM
                  (X_CHOOSE_THEN (parse_term @"e:num") SUBST1_TAC 
                   << REWRITE_RULE [LE_EXISTS])
           |> THEN <| SIMP_TAC [ADD_SUB2
                                GSYM NOT_LE
                                LE_ADD; EQ_ADD_LCANCEL]
           |> THEN <| MESON_TAC [])
  
  let SUB_ELIM_THM' = 
      prove
  
negative.code: (* ------------------------------------------------------------------------- *)
  (* Useful "without loss of generality" lemmas.                               *)
  (* ------------------------------------------------------------------------- *)
  
  let WLOG_LE = 
      prove
          ((parse_term @"(!m n. P m n <=> P n m) /\ (!m n. m <= n ==> P m n) ==> !m n. P m n"), 
  