let x, y be real number ; :: thesis: (x |^ 3) - (y |^ 3) = (x - y) * (((x ^2 ) + (x * y)) + (y ^2 ))
(x - y) * (((x ^2 ) + (x * y)) + (y ^2 )) = (((x * (x ^2 )) + ((x * x) * y)) + (x * (y ^2 ))) - (((y * (x ^2 )) + ((y * x) * y)) + (y * (y ^2 )))
.= (((x * (x |^ 2)) + ((x * x) * y)) + (x * (y ^2 ))) - (((y * (x ^2 )) + ((y * x) * y)) + (y * (y ^2 ))) by NEWTON:100
.= (((x |^ (2 + 1)) + ((x * x) * y)) + (x * (y ^2 ))) - (((y * (x ^2 )) + ((y * x) * y)) + (y * (y ^2 ))) by NEWTON:11
.= (((x |^ 3) + (x * (y * y))) - ((y * x) * y)) - (y * (y ^2 ))
.= (x |^ 3) - ((y |^ 2) * y) by NEWTON:100
.= (x |^ 3) - (y |^ (2 + 1)) by NEWTON:11 ;
hence (x |^ 3) - (y |^ 3) = (x - y) * (((x ^2 ) + (x * y)) + (y ^2 )) ; :: thesis: verum