for n being positive Integer holds
( n + 1 divides (n ^2) + 1 iff n = 1 )