NUM_CANCEL_CONV : term -> thm
|- t1 + ... + tn = s1 + ... + sm <=> u1 + ... + uk = v1 + ... + vl
# 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