for a, b, c being Nat
for p being non trivial Nat st not a divides b holds
(p |^ a) |^ c <> p |^ b