anchor.diff:      prove
           ((parse_term @"!f s. sum (support (+) f s) f = sum s f"), 
            SIMP_TAC [sum; iterate; SUPPORT_SUPPORT])
  +
   let SUM_ADD = 
       prove
           ((parse_term @"!f g s. FINITE s ==> (sum s (\x. f(x) + g(x)) = sum s f + sum s g)"), 
  
positive.code:              |> THEN 
               <| ASM_REWRITE_TAC [ARITH_RULE(parse_term @"a + 1 <= b <=> a < b")]])
  
  let NSUM_UNION_EQ = prove((parse_term @"!s t u. FINITE u /\ (s INTER t = {}) /\ (s UNION t = u)
             ==> (nsum s f + nsum t f = nsum u f)"), MESON_TAC [NSUM_UNION; DISJOINT; FINITE_SUBSET; SUBSET_UNION])
  
  let NSUM_EQ_SUPERSET = prove((parse_term @"!f s t:A->bool.
          FINITE t /\ t SUBSET s /\
          (!x. x IN t ==> (f x = g x)) /\
          (!x. x IN s /\ ~(x IN t) ==> (f(x) = 0))
  
negative.code: (* ------------------------------------------------------------------------- *)
  (* Sums of natural numbers.                                                  *)
  (* ------------------------------------------------------------------------- *)
  
  let nsum = new_definition(parse_term @"nsum = iterate (+)")
  
  let NEUTRAL_ADD = 
  