let a, b be odd Integer; :: thesis: ( a - b is square implies not a + b is square )
assume a - b is square ; :: thesis: not a + b is square
then consider c being Nat such that
A1: c ^2 = a - b by PYTHTRIP:def 3;
reconsider c = c as even Nat by A1;
A2: ( |.a.| in NAT & |.b.| in NAT ) by INT_1:3;
then reconsider k = max (|.a.|,|.b.|) as odd Nat by XXREAL_0:def 10;
reconsider l = min (|.a.|,|.b.|) as odd Nat by A2, XXREAL_0:def 9;
A3: |.a.| + |.b.| = k + l by NEWTON03:41;
2 divides c by ABIAN:def 1;
then 2 * 2 divides c * c by NEWTON02:2;
then A5: 2 * 2 divides c ^2 by SQUARE_1:def 1;

per cases ( |.(a + b).| = |.a.| + |.b.| or |.(a - b).| = |.a.| + |.b.| ) by ABS;

suppose B1: |.(a + b).| = |.a.| + |.b.| ; :: thesis: not a + b is square

then B2: |.(a - b).| = |.(|.a.| - |.b.|).| by LABS
.= k - l by MMD ;
not 4 divides (k |^ 1) + (l |^ 1) by A1, A5, B2, NEWTON03:20;
hence not a + b is square by B1, A3, A4I; :: thesis: verum

end;

suppose B1: |.(a - b).| = |.a.| + |.b.| ; :: thesis: not a + b is square

then B2: |.(a + b).| = |.(|.a.| - |.b.|).| by LmABS
.= k - l by MMD ;
4 divides (k |^ 1) + (l |^ 1) by B1, A1, NEWTON03:41, A5;
then not 4 divides k - l by NEWTON03:20;
hence not a + b is square by B2, A4I; :: thesis: verum

end;

end;