theorem :: NEWTON03:63

for a, b being non zero Nat
for n being non trivial Nat holds (a + b) |-count ((a |^ n) + (b |^ n)) < n