theorem MO5: :: NEWTON06:65

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