let a, b be Nat; ( a is odd & b is odd implies 8 divides (a |^ 2) - (b |^ 2) )
assume A0:
( a is odd & b is odd )
; 8 divides (a |^ 2) - (b |^ 2)
then consider k being Nat such that
A1:
a = (2 * k) + 1
by ABIAN:9;
consider n being Nat such that
A1a:
b = (2 * n) + 1
by A0, ABIAN:9;
( ( k is even or k + 1 is even ) & ( n is even or n + 1 is even ) )
;
then
(k * (k + 1)) - (n * (n + 1)) is even
;
then A2:
2 * 4 divides 4 * ((k * (k + 1)) - (n * (n + 1)))
by INT_6:8;
(a |^ 2) - (b |^ 2) =
(((2 * k) + 1) |^ 2) - (((4 * n) * (n + 1)) + 1)
by A1, A1a, Th62
.=
(((4 * k) * (k + 1)) + 1) - (((4 * n) * (n + 1)) + 1)
by Th62
.=
4 * ((k * (k + 1)) - (n * (n + 1)))
;
hence
8 divides (a |^ 2) - (b |^ 2)
by A2; verum