let n be non zero Nat; :: thesis: n - ((n div 2) * 2) <= 1
A2: n = (2 * (n div 2)) + (n mod 2) by NAT_D:2;

per cases ( n mod 2 = 0 or n mod 2 = 1 ) by NAT_1:23, NAT_D:1;

suppose n mod 2 = 0 ; :: thesis: n - ((n div 2) * 2) <= 1

hence n - ((n div 2) * 2) <= 1 by A2; :: thesis: verum

end;

suppose n mod 2 = 1 ; :: thesis: n - ((n div 2) * 2) <= 1

hence n - ((n div 2) * 2) <= 1 by A2; :: thesis: verum

end;

end;