for a, b being odd Integer holds Parity (a + b) = 2 * (Parity (((a div 2) + (b div 2)) + 1))