for a, b being non zero Nat
for n being odd Nat holds ((a |^ (n + 2)) + (b |^ (n + 2))) / (a + b) = ((a |^ (n + 1)) + (b |^ (n + 1))) - ((a * b) * (((a |^ n) + (b |^ n)) / (a + b)))