theorem SAB: :: NEWTON05:93

for a, b being Integer holds a + b = ((2 * ((a div 2) + (b div 2))) + (parity a)) + (parity b)