let i, j be odd Nat; :: thesis: ( i <= j implies ex k being Nat st i + (2 * k) = j )

assume i <= j ; :: thesis: ex k being Nat st i + (2 * k) = j

then consider jjj being Nat such that

A1: j = i + jjj by NAT_1:10;

jjj is even by A1;

then consider jj being Nat such that

A2: 2 * jj = jjj by ABIAN:def 2;

take jj ; :: thesis: i + (2 * jj) = j

thus i + (2 * jj) = j by A1, A2; :: thesis: verum

assume i <= j ; :: thesis: ex k being Nat st i + (2 * k) = j

then consider jjj being Nat such that

A1: j = i + jjj by NAT_1:10;

jjj is even by A1;

then consider jj being Nat such that

A2: 2 * jj = jjj by ABIAN:def 2;

take jj ; :: thesis: i + (2 * jj) = j

thus i + (2 * jj) = j by A1, A2; :: thesis: verum