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