let a, b, m be Nat; :: thesis: for t being Integer holds
( (a |^ (m + 1)) - (b |^ (m + 1)) = ((a - b) * (((t * (a + b)) + (a |^ m)) + (b |^ m))) / 2 iff (a |^ m) - (b |^ m) = (a - b) * t )
let t be Integer; :: thesis: ( (a |^ (m + 1)) - (b |^ (m + 1)) = ((a - b) * (((t * (a + b)) + (a |^ m)) + (b |^ m))) / 2 iff (a |^ m) - (b |^ m) = (a - b) * t )
( a + b = 0 implies (a |^ m) - (b |^ m) = (a - b) * t )

proof

assume a + b = 0 ; :: thesis: (a |^ m) - (b |^ m) = (a - b) * t
then ( a = 0 & b = 0 ) ;
hence (a |^ m) - (b |^ m) = (a - b) * t ; :: thesis: verum

end;

hence ( (a |^ (m + 1)) - (b |^ (m + 1)) = ((a - b) * (((t * (a + b)) + (a |^ m)) + (b |^ m))) / 2 iff (a |^ m) - (b |^ m) = (a - b) * t ) by Lm16, Lm17; :: thesis: verum