Solution (source code)

= Solution

Consider one iteration with $a_i>b_i>0$ and $r_i=a_i\bmod b_i$. If $b_i\le a_i/2$, then $r_i<b_i\le a_i/2$. If $b_i>a_i/2$, the <quotient> is $1$, so $r_i=a_i-b_i<a_i/2$. In either case $r_i<a_i/2$, whence
$$
a_{i+1}b_{i+1}=b_ir_i<\frac{a_ib_i}{2}.
$$
Repeated application, or <mathematical induction>, proves
$$
\boxed{a_nb_n<\frac{ab}{2^n}\qquad(n\ge1\text{ performed iterations}).}
$$
This also holds for the final iteration, whose left side is zero. For zero iterations the correct relation is equality $a_0b_0=ab$, rather than a strict <inequality>.