let n be Nat; :: thesis: ex m being Element of NAT st

( n = 2 * m or n = (2 * m) + 1 )

take n div 2 ; :: thesis: ( n = 2 * (n div 2) or n = (2 * (n div 2)) + 1 )

set k = n mod 2;

A1: ( n mod 2 = 0 or n mod 2 = 1 )

hence ( n = 2 * (n div 2) or n = (2 * (n div 2)) + 1 ) by A1; :: thesis: verum

( n = 2 * m or n = (2 * m) + 1 )

take n div 2 ; :: thesis: ( n = 2 * (n div 2) or n = (2 * (n div 2)) + 1 )

set k = n mod 2;

A1: ( n mod 2 = 0 or n mod 2 = 1 )

proof

n = (2 * (n div 2)) + (n mod 2)
by NAT_D:2;
n mod 2 < 1 + 1
by NAT_D:1;

then A2: n mod 2 <= 0 + 1 by NAT_1:13;

end;then A2: n mod 2 <= 0 + 1 by NAT_1:13;

now :: thesis: ( n mod 2 = 0 or n mod 2 = 1 )

hence
( n mod 2 = 0 or n mod 2 = 1 )
; :: thesis: verumend;

hence ( n = 2 * (n div 2) or n = (2 * (n div 2)) + 1 ) by A1; :: thesis: verum