let a, b be odd Nat; :: thesis: ( a <> b implies 1 = min ((2 |-count (a - b)),(2 |-count (a + b))) )
assume A0: a <> b ; :: thesis: 1 = min ((2 |-count (a - b)),(2 |-count (a + b)))
reconsider k = |.(a - b).| as even Nat ;
reconsider l = a + b as even Nat ;
A1: 2 |^ 2 = 2 * 2 by NEWTON:81;
A2: ( 2 |^ 1 divides |.(a - b).| & 2 |^ 1 divides a + b ) by ABIAN:def 1;
A3: a - b <> b - b by A0;
then A4: ( 2 |-count |.(a - b).| <> 0 & 2 |-count (a + b) <> 0 ) by A2, NAT_3:27;

per cases ( not 4 divides a - b or 4 divides a - b ) ;

suppose not 4 divides a - b ; :: thesis: 1 = min ((2 |-count (a - b)),(2 |-count (a + b)))

then not |.(2 |^ (1 + 1)).| divides |.(a - b).| by A1, INT_2:16;
then 1 = 2 |-count |.(a - b).| by A2, A3, NAT_3:def 7;
hence 1 = min ((2 |-count (a - b)),(2 |-count (a + b))) by A4, NAT_1:14, XXREAL_0:def 9; :: thesis: verum

end;

suppose 4 divides a - b ; :: thesis: 1 = min ((2 |-count (a - b)),(2 |-count (a + b)))

then not 2 |^ (1 + 1) divides a + b by A1, NEWTON02:58;
then 2 |-count (a + b) = 1 by A2, NAT_3:def 7;
hence 1 = min ((2 |-count (a - b)),(2 |-count (a + b))) by A4, NAT_1:14, XXREAL_0:def 9; :: thesis: verum

end;

end;