c++algorithm integer-overflow correctness proof-of-correctness

Correctness of multiplication with overflow detection

The following C++ template detects overflows from multiplying two unsigned integers.

template<typename UInt> UInt safe_multiply(UInt a, UInt b) {
    UInt x = a * b; // x := ab mod n, for n := 2^#bits > 0
    if (a != 0 && x / a != b)
        cerr << "Overflow for " << a << " * " << b << "." << endl;
    return x;
}

Can you give a proof that this algorithm detects every potential overflow, regardless of how many bits UInt uses?

The case
$a=0\lor b=0$

cannot result in overflows, so we can consider
$a,b,n\in\mathbb{N}_{>0}$ .

It seems that the correctness proof boils down to leading
$\left\lfloor\frac{ab \mod n}{a}\right\rfloor=b~\land~ab\ge n$

to a contradiction, since x / a actually means $\left\lfloor\frac{x}{a}\right\rfloor$ .

When assuming
$\left\lfloor\frac{x}{a}\right\rfloor=\frac{x}{a}$

, this leads to the straightforward consequence
$\left\lfloor\frac{x}{a}\right\rfloor=b\Leftrightarrow\frac{x}{a}=b\Leftrightarrow ab \mod n=ab$

thus
$ab\mod n=ab\ge n$

which contradicts n > 0.

So it remains to show
$\left\lfloor\frac{ab \mod n}{a}\right\rfloor=\frac{ab \mod n}{a}$

or there must be another way.

If the last equation is true, WolframAlpha fails to confirm that (also with exponents).
However, it asserts that the original assumptions have no integer solutions, so the algorithms seems to be correct indeed.
But it doesn't provide an explanation. So why is it correct?

I am looking for the smallest possible explanation that is still mathematically profound, ideally that it fits in a single-line comment. Maybe I am missing something trivial, or the problem is not as easy as it looks.

On a side note, I used Codecogs Equation Editor for the LaTeX markup images, which apparently looks bad in dark mode, so consider switching to light mode or, if you know, please tell me how to use different images depending on the client settings. It is just \bg{white} vs. \bg{black} as part of the image URLs.

Solution

To be clear, I'll use the multiplication and division symbols (*, /) mathematically.

Also, for convenience let's name the set N = {0, 1, ..., n - 1}.

Let's clear up what unsigned multiplication is:
Unsigned multiplication for some magnitude, n, is a modular n operation on unsigned-n inputs (inputs that are in N) that results in an unsigned-n output (ie. also in N).
In other words, the result of unsigned multiplication, x, is x = a*b (mod n), and, additionally, we know that x,a,b are in N.
It's important to be able to expand many modular formulas like so: x = a*b - k*n, where k is an integer - but in our case x,a,b are in N so this implies that k is in N.

Now, let's mathematically say what we're trying to prove:
Given positive integers, a,n, and non-negative integers x,b, where x,a,b are in N, and x = a*b (mod n), then a*b >= n (overflow) implies floor(x/a) != b.

Proof:

If overflow (a*b >= n) then x >= n - k*n = (1 - k)*n (for k in N),
As x < n then (1 - k)*n < n, so k > 0.
This means x <= a*b - n.

So, floor(x/a) <= floor([a*b - n]/a) = floor(a*b/a - n/a) = b - floor(n/a) <= b - 1,
Abbreviated: floor(x/a) <= b - 1
Therefore floor(x/a) != b