theorem :: NEWTON06:78

for a, b being odd Nat holds
( not a,b are_coprime or (((a |^ 4) + (b |^ 4)) / 2) mod 5 = 3 or (((a |^ 4) + (b |^ 4)) / 2) mod 5 = 1 )