theorem :: NEWTON03:104

for a, b being non zero Integer
for p being odd prime Nat st |.a.| <> |.b.| & not p divides b holds
p |-count ((a |^ 2) - (b |^ 2)) = max ((p |-count (a - b)),(p |-count (a + b)))