for n, k being Nat
for a being non trivial Nat holds Py (a,n) divides Py (a,(n * k))