>>679
679は自分で書かないで卑怯もいいところだが、679には
∃n ∀N [ (n^2 < N ∧ N < n(n+1)) → Comp(N) ]

For ∃n, ∀N [ (n^2 < N ∧ N < n(n+1)) → Comp(N) ]
の違いが分からないらしい。病院に行った方がいい。