I'm trying to reduce one calculation in an iterative Successive Over-Relaxation procedure for a program I'm writing. The code that works does this calculation:

$$
s = \left\lfloor\frac{b + \left\lfloor\frac{2^{16}-1}{4}\right\rfloor}{\left\lfloor\frac{2^{16}}{4}\right\rfloor}\right\rfloor
$$

Now, I *think* that the following two properties of floors/ceilings and modulus division hold up (or at least I couldn't find a contradicting set of inputs):

$$
\forall x\in\mathbb{N},y\in\mathbb{N}\left(\left\lfloor\frac{x-1}{y}\right\rfloor = \frac{x-y}{y} \leftrightarrow x\mod y = 0\right)\\
\forall x\in\mathbb{N},y\in\mathbb{N}\left(\left\lfloor\frac{x+y-1}{y}\right\rfloor=\left\lceil\frac{x}{y}\right\rceil\right)
$$

So, according to the first property, because $2^{16}\mod4=0$, I can rewrite the above as:

$$
s=\left\lfloor\frac{b+\frac{2^{16}-4}{4}}{\left\lfloor\frac{2^{16}}{4}\right\rfloor}\right\rfloor = \left\lfloor\frac{b+\frac{2^{16}}{4}-1}{\left\lfloor\frac{2^{16}}{4}\right\rfloor}\right\rfloor
$$

and since, again, $2^{16}\mod4=0$, it must be true that $\frac{2^{16}}{4}=\left\lfloor\frac{2^{16}}{4}\right\rfloor$, and so by the second property this can be re-written as:

$$
s=\left\lceil\frac{b}{\frac{2^{16}}{4}}\right\rceil = \left\lceil\frac{b}{2^{14}}\right\rceil
$$

This *usually* gets me the right answer, but sometimes I get erroneous outputs, and I'm trying to eliminate this simplification of the original as the cause. Are those two properties really true? Or did I mess up in the actual simplification somewhere? Or is it actually fine and the flaw is probably elsewhere?

Bonus Question
--------------

Should those statements above be written as $\forall x\in\mathbb{N},y\in\mathbb{N}$ or $\forall(x,y)\in\mathbb{N}^2$? Or are those equivalent? I'll edit my question as appropriate/if needed according to any comments on the formatting.