for n being Nat
for t, z being Integer holds t * z divides (((t + z) |^ n) - ((t - z) |^ n)) + (((- z) |^ n) - (z |^ n))