for a being non zero square Element of NAT
for p being prime Nat st a + p is square holds
p = (2 * (sqrt a)) + 1