theorem :: NEWTON01:16

for a, b being Nat holds (a |^ 3) - (b |^ 3) = ((a - b) * ((((a + b) * (a + b)) + (a |^ 2)) + (b |^ 2))) / 2