theorem npcan (a b: nat): $ b <= a -> a - b + b = a $;
a - b + b = b + (a - b)
b <= a -> b + (a - b) = a
b <= a -> a - b + b = a