let a, b be odd Integer; :: thesis: Parity (a + b) = 2 * (Parity (((a div 2) + (b div 2)) + 1))
( parity a = 1 & parity b = 1 ) by NAT_2:def 1;
then Parity (a + b) = Parity (((2 * ((a div 2) + (b div 2))) + 1) + 1) by SAB
.= Parity (2 * (((a div 2) + (b div 2)) + 1))
.= (Parity 2) * (Parity (((a div 2) + (b div 2)) + 1)) by ILP ;
hence Parity (a + b) = 2 * (Parity (((a div 2) + (b div 2)) + 1)) ; :: thesis: verum