how can I do a formal proof of the following description:
$a\;div\;b = \begin{cases} \lfloor \frac{a}{b} \rfloor &\text{ if }b>0\\ \lceil \frac{a}{b} \rceil &\text{ if }b<0 \end{cases}\\$
It seems pretty straight forward as $a$ div $b$ is defined as $q$ from the expression $a=q b + r$, where r has to be a positive integer smaller than b.