for a being Nat
for s, z being non zero Nat holds a divides (a |^ s) + (a |^ z)