let a, b, n be Nat; :: thesis: ( a + b divides (a |^ n) - (b |^ n) implies a + b divides (a |^ (n + 1)) + (b |^ (n + 1)) )
assume a + b divides (a |^ n) - (b |^ n) ; :: thesis: a + b divides (a |^ (n + 1)) + (b |^ (n + 1))
then a + b divides (a * ((a |^ n) + 0)) + (b * ((b |^ n) + 0)) by Th31;
then a + b divides (a |^ (n + 1)) + (b * (b |^ n)) by NEWTON:6;
hence a + b divides (a |^ (n + 1)) + (b |^ (n + 1)) by NEWTON:6; :: thesis: verum