for n being Nat
for a being non trivial Nat holds Py (a,n) >= n