theorem :: NEWTON06:79
for a, b being Nat st a,b are_coprime holds
((a |^ 4) - (b |^ 4)) mod 5 is square