let a be odd Nat; :: thesis: Parity (a - 1) = 2 * (Parity (a div 2))
a = ((a div 2) * 2) + (a mod 2) by INT_1:59
.= ((a div 2) * 2) + 1 by NAT_D:12 ;
then Parity (a - 1) = (Parity (a div 2)) * (Parity 2) by ILP;
hence Parity (a - 1) = 2 * (Parity (a div 2)) ; :: thesis: verum