let a, b be odd Integer; 2 |-count ((a |^ 2) + (b |^ 2)) = 1
reconsider t = a |^ 2, u = b |^ 2 as odd Nat ;
A2:
2 * 2 = 2 |^ 2
by NEWTON:81;
( 2 divides a - b & 2 divides a + b )
by ABIAN:def 1;
then
2 * 2 divides (a - b) * (a + b)
by NAT31;
then
4 divides (a |^ 2) - (b |^ 2)
by NEWTON01:1;
then
( 2 |^ 1 divides (a |^ 2) + (b |^ 2) & not 2 |^ (1 + 1) divides (a |^ 2) + (b |^ 2) )
by ABIAN:def 1, A2, NEWTON0258;
hence
2 |-count ((a |^ 2) + (b |^ 2)) = 1
by NAT_3:def 7; verum