<s>[INST] Question regarding floor function subtraction Let:


*

*$a,b,c$ be integers with $a \ge b$ and $c > 0$
There exists integers $s,t$ such that:
$$\left\lfloor\frac{a}{c}\right\rfloor = \frac{a - s}{c}\text{  },\text{  }\left\lfloor\frac{b}{c}\right\rfloor = \frac{b-t}{c}$$
Does it follow that:
$$\left\lfloor\frac{a}{c}\right\rfloor - \left\lfloor\frac{b}{c}\right\rfloor = \left\lfloor\frac{a-b}{c}\right\rfloor  \iff s \ge t$$
Here's my thinking:
If $s \ge t$, then  $c > (s-t) \ge 0$ and:
$$\left\lfloor\frac{a}{c}\right\rfloor - \left\lfloor\frac{b}{c}\right\rfloor = \frac{a - b - (s-t)}{c} = \left\lfloor\frac{a-b}{c}\right\rfloor$$
If $s < t$, then $0 > (s-t) > -c$ and:
$$\frac{a - b - (s-t)}{c} = \frac{a - b - (s-t)}{c} = \left\lfloor\frac{a-b}{c}\right\rfloor + 1$$
Did I make a mistake?  If I did not make a mistake, is there a simpler argument?
 [/INST] What you've done looks correct. Here's a somewhat different way to show it, although not really much simpler, but it does include a few points you don't show explicitly. Note you can use a similar proof in the case $c \lt 0$ to confirm your proposition, but you would need to change it to use $s \le t$ instead.
You have by Euclidean division that for some unique integer $m$, there is an integer $r$ such that
$$a = mc + r, \; 0 \le r \lt c \tag{1}\label{eq1A}$$
Thus, you then have
$$m = \left\lfloor\frac{a}{c}\right\rfloor = \frac{a - s}{c} \implies a = mc + s \tag{2}\label{eq2A}$$
This means that $s$ is uniquely the value of $r$ in \eqref{eq1A}. Similarly, this means for some unique integer $n$
$$\left\lfloor\frac{b}{c}\right\rfloor = \frac{b-t}{c} = n \implies b = cn + t, \; 0 \le t \lt c \tag{3}\label{eq3A}$$
As for your proposition of
$$\left\lfloor\frac{a}{c}\right\rfloor - \left\lfloor\frac{b}{c}\right\rfloor = \left\lfloor\frac{a-b}{c}\right\rfloor  \iff s \ge t \tag{4}\label{eq4A}$$
note you have
$$m - n = \left\lfloor\frac{(m-n)c + s - t}{c}\right\rfloor = m - n + \left\lfloor\frac{s - t}{c}\right\rfloor \iff \left\lfloor\frac{s - t}{c}\right\rfloor = 0 \iff s \ge t \tag{5}\label{eq5A}$$
</s>