theorem addb00 (a b: nat): $ b0 a + b0 b = b0 (a + b) $;
a + a + (b + b) = a + b + (a + b)
b0 a + b0 b = b0 (a + b)