NUM_CANCEL_CONV : term -> thm

SYNOPSIS
Cancels identical terms from both sides of natural number equation.

DESCRIPTION
Given an equational term `t1 + ... + tn = s1 + ... + sm` (with arbitrary association of the additions) where both sides have natural number type, the conversion identifies common elements among the ti and si, and cancels them from both sides, returning a theorem:
  |- t1 + ... + tn = s1 + ... + sm <=> u1 + ... + uk = v1 + ... + vl
where the ui and vi are the remaining elements of the ti and si respectively, in some order.

FAILURE CONDITIONS
Fails if applied to a term that is not an equation between natural number terms.

EXAMPLE
  # NUM_CANCEL_CONV `(a + b + x * y + SUC c) + d = SUC c + d + y * z`;;
  val it : thm =
    |- (a + b + x * y + SUC c) + d = SUC c + d + y * z <=>
       x * y + b + a = y * z

USES
Simplifying equations where explicitly directing the cancellation would be tedious. However, this is mostly intended for ``bootstrapping'', before more powerful rules like ARITH_RULE and NUM_RING are available.

SEE ALSO
ARITH_RULE, ARITH_TAC, NUM_RING.