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