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