let a, b be Integer; :: thesis: a + b = ((2 * ((a div 2) + (b div 2))) + (parity a)) + (parity b)
( a = ((a div 2) * 2) + (a mod 2) & b = ((b div 2) * 2) + (b mod 2) ) by INT_1:59;
hence a + b = ((2 * ((a div 2) + (b div 2))) + (parity a)) + (parity b) ; :: thesis: verum