View source for Integer division that rounds up

== Introduction == 

Usual integer division rounds down: <math>\frac ab = \left \lfloor \frac ab \right \rfloor</math> for <math>a,b \in \mathbb N, b\neq 0</math>. To round up (if overflow is not an issue), you can use following algorithm with the usual roundig down division:
<math>
q = \frac{x+y-1}{y} = \left \lceil \frac xy \right \rceil
</math>

== Proof ==

Proof is in two parts; 1st if <math>y</math> divides <math>x</math>, and if not. Note that usual integer division rounds down.

'''Part 1'''. If <math>y</math> divides <math>x</math> we have <math>x=ay</math> for some <math>a\in\mathbb N_+</math>. Thus we have

<math>
\begin{align}
\left \lfloor  \frac{x+y-1}{y} \right \rfloor 
&=
\left \lfloor  \frac{x}{y} + \frac{y-1}y \right \rfloor  \\
&=
\left \lfloor  \frac{ay}{y} + \frac{y-1}y \right \rfloor  \\
&=
\frac{ay}{y} \\
&=
\frac{x}{y}
\end{align}
</math>

because <math>0 \leq \frac{y-1}y < 1</math>. This part is ok.

'''Part 2'''. If <math>y</math> does not divide <math>x</math> we have <math>x=by + r</math> for some <math>b\in\mathbb N_+</math> and <math>0<r<b</math>. Thus we have

<math>
\begin{align}
\left \lfloor  \frac{x+y-1}{y} \right \rfloor 
&=
\left \lfloor  \frac{x}{y} + \frac{y-1}y \right \rfloor  \\
&=
\left \lfloor  \frac{by+r}{y} + \frac{y-1}y \right \rfloor  \\
&=
\left \lfloor  \frac{by}{y} + \frac ry + \frac yy - \frac 1y \right \rfloor  \\
&=
\left \lfloor  \frac{by + y}{y} + \frac {r-1}y  \right \rfloor  \\
&=
\left \lfloor  \frac{(b+1)y}{y} + \frac {r-1}y  \right \rfloor  \\
&=
\frac{(b+1)y}{y} \\
\end{align}
</math>

Which is one greater (the ceiling).

'''Combine''' the results, and we have
<math>
\left \lfloor  \frac{x+y-1}{y} \right \rfloor 
=
\left \lceil \frac{x}{y} \right \rceil
</math>
which was the question.

== References ==

https://math.stackexchange.com/questions/2591316/proof-for-integer-division-algorithm-that-rounds-up

For more details, see Algorithmic problem solving by R Backhouse 2011, Exercise 15.12 (following the definition 15.22).