\begin{definition}[Definition:Remainder/Real]
Let $x, y \in \R$ be real numbers such that $y \ne 0$.
The '''remainder of $x$ on division by $y$''' is defined as the value of $r$ in the expression:
:$\forall x, y \in \R, y \ne 0: \exists! q \in \Z, r \in \R: x = q y + r, 0 \le r < \size y$
From the definition of the Modulo Operation:
:$x \bmod y := x - y \floor {\dfrac x y}$
it can be seen that the '''remainder of $x$ on division by $y$''' is defined as:
:$r = x \bmod y$
\end{definition}