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.