for p being prime Nat
for a, b being Integer st |.a.| <> |.b.| holds
p |-count ((a |^ 2) - (b |^ 2)) = (p |-count (a - b)) + (p |-count (a + b))