for p being Prime holds NatDivisors (p * p) = {1,p,(p * p)}