let a be Nat; :: thesis: ( a is even & not 4 divides a implies ex b being Nat st

( b = a / 2 & b is odd ) )

assume A1: ( a is even & not 4 divides a ) ; :: thesis: ex b being Nat st

( b = a / 2 & b is odd )

then consider b being Nat such that

A2: a = 2 * b ;

not 2 * 2 divides 2 * b by A1, A2;

then ( b = a / 2 & b is odd ) by A2, LmGCD;

hence ex b being Nat st

( b = a / 2 & b is odd ) ; :: thesis: verum

( b = a / 2 & b is odd ) )

assume A1: ( a is even & not 4 divides a ) ; :: thesis: ex b being Nat st

( b = a / 2 & b is odd )

then consider b being Nat such that

A2: a = 2 * b ;

not 2 * 2 divides 2 * b by A1, A2;

then ( b = a / 2 & b is odd ) by A2, LmGCD;

hence ex b being Nat st

( b = a / 2 & b is odd ) ; :: thesis: verum