theorem shladd (a b c: nat): $ shl (a + b) c = shl a c + shl b c $;
(a + b) * 2 ^ c = a * 2 ^ c + b * 2 ^ c
shl (a + b) c = shl a c + shl b c