let a, b be Nat; :: thesis: (a |^ 3) - (b |^ 3) = ((a - b) * ((((a + b) * (a + b)) + (a |^ 2)) + (b |^ 2))) / 2
A1: (a |^ 2) - (b |^ 2) = (a - b) * (a + b) by Th1;
(a |^ 3) - (b |^ 3) = (a |^ (2 + 1)) - (b |^ (2 + 1))
.= ((a - b) * ((((a + b) * (a + b)) + (a |^ 2)) + (b |^ 2))) / 2 by A1, Th14 ;
hence (a |^ 3) - (b |^ 3) = ((a - b) * ((((a + b) * (a + b)) + (a |^ 2)) + (b |^ 2))) / 2 ; :: thesis: verum