let a be odd Nat; :: thesis: ( Parity (a + 1) = 2 iff parity (a div 2) = 0 )
a >= 1 by NAT_1:14;

per cases then ( a = 1 or a > 1 ) by XXREAL_0:1;

suppose B0: a = 1 ; :: thesis: ( Parity (a + 1) = 2 iff parity (a div 2) = 0 )

parity (1 div (1 + 1)) = parity 0 ;
hence ( Parity (a + 1) = 2 iff parity (a div 2) = 0 ) by B0; :: thesis: verum

end;

suppose a > 1 ; :: thesis: ( Parity (a + 1) = 2 iff parity (a div 2) = 0 )

then reconsider a = a as non trivial odd Nat by NAT_2:def 1;
reconsider l = (2 * 0) + 1 as odd Nat ;
L1: ( Parity (a + 1) = 2 implies parity (a div 2) = 0 )

proof

assume A1: Parity (a + 1) = 2 ; :: thesis: parity (a div 2) = 0

per cases then ( 2 = min ((Parity (l + 1)),(Parity (a - 1))) or 2 >= 2 * (Parity (l + 1)) ) by PMG;

suppose 2 = min ((Parity (l + 1)),(Parity (a - 1))) ; :: thesis: parity (a div 2) = 0

then Parity (a - 1) > 2 by A1, PSD, XXREAL_0:def 9;
then 2 |^ (2 |-count (a - 1)) > 2 |^ 1 by Def1;
then 2 |-count (a - 1) > 1 by PREPOWER:93;
then 2 |-count (a - 1) >= 1 + 1 by NAT_1:13;
then 2 |^ 2 divides a - 1 by NEWTON03:59;
then 2 * 2 divides a - 1 by NEWTON:81;
then ((a - 1) div 4) * 4 = a - 1 by NAT_D:3
.= (((a div 2) * 2) + (a mod 2)) - 1 by INT_1:59
.= (((a div 2) * 2) + 1) - 1 by NAT_D:12 ;
then ((a - 1) div 4) * 2 = a div 2 ;
hence parity (a div 2) = 0 ; :: thesis: verum

end;

suppose 2 >= 2 * (Parity (l + 1)) ; :: thesis: parity (a div 2) = 0

hence parity (a div 2) = 0 ; :: thesis: verum

end;

end;

end;

( parity (a div 2) = 0 implies Parity (a + 1) = 2 )

proof

assume parity (a div 2) = 0 ; :: thesis: Parity (a + 1) = 2
then reconsider k = a div 2 as even Nat ;
a + 1 = (((a div 2) * 2) + (a mod 2)) + 1 by INT_1:59
.= (((a div 2) * 2) + 1) + 1 by NAT_D:12
.= 2 * (k + 1) ;
then Parity (a + 1) = (Parity 2) * (Parity (k + 1)) by ILP
.= 2 * 1 ;
hence Parity (a + 1) = 2 ; :: thesis: verum

end;

hence ( Parity (a + 1) = 2 iff parity (a div 2) = 0 ) by L1; :: thesis: verum

end;

end;