The theorem that "I mean" is

∀a. ∃b. ∀x. ∀y. (a+b)·(a+b) != SS((SSx)·(SSy))

In words:

For any number a, there is a number b, so that for all pairs of numbers, call them x and y, the number a+b squared isn't twice the successor of the product of twice the successor of x and trice the successor of y.

If you define B=a+b, X=x+2 and Y=y+2, the thing reads

B^2-2 != X·Y

I.e. B^2-2 can't be factorized into any X and Y.

And I'm pretty sure that what it comes down to, yes :)