let a, b be odd Integer; :: thesis: ( Parity (a + b) = 2 iff parity (a div 2) = parity (b div 2) )
thus ( Parity (a + b) = 2 implies parity (a div 2) = parity (b div 2) ) :: thesis: ( parity (a div 2) = parity (b div 2) implies Parity (a + b) = 2 )

proof

assume Parity (a + b) = 2 ; :: thesis: parity (a div 2) = parity (b div 2)
then 2 * (Parity (((a div 2) + (b div 2)) + 1)) = 2 * 1 by SPA;
then (a div 2) + (b div 2) is even ;
hence parity (a div 2) = parity (b div 2) by EVP; :: thesis: verum

end;

assume parity (a div 2) = parity (b div 2) ; :: thesis: Parity (a + b) = 2
then ( a div 2 is odd iff b div 2 is odd ) ;
then 2 * (Parity (((a div 2) + (b div 2)) + 1)) = 2 * 1 by NAT_2:def 1;
hence Parity (a + b) = 2 by SPA; :: thesis: verum