let a, b be Nat; :: thesis: a - b divides (a |^ 0) - (b |^ 0)
(a |^ 0) - (b |^ 0) = 1 - (b |^ 0) by NEWTON:4
.= 1 - 1 by NEWTON:4 ;
hence a - b divides (a |^ 0) - (b |^ 0) by INT_2:12; :: thesis: verum