let n be odd Nat; :: thesis: ( n <= 2 implies n = 1 )

assume A1: n <= 2 ; :: thesis: n = 1

n <> 2 * 1 ;

then n < 1 + 1 by A1, XXREAL_0:1;

then A2: n <= 1 by NAT_1:13;

n >= 1 by ABIAN:12;

hence n = 1 by A2, XXREAL_0:1; :: thesis: verum

assume A1: n <= 2 ; :: thesis: n = 1

n <> 2 * 1 ;

then n < 1 + 1 by A1, XXREAL_0:1;

then A2: n <= 1 by NAT_1:13;

n >= 1 by ABIAN:12;

hence n = 1 by A2, XXREAL_0:1; :: thesis: verum