for c, k being Nat
for a, b being non zero Nat st c >= a + b holds
(c |^ (k + 1)) * (a + b) > (a |^ (k + 2)) + (b |^ (k + 2))