The q and r computed by the extracts of these theorems are not the same as those returned by the

Here, things are set up so that the same inequalities for r are satisfied over 2 adjacent quadrants of a,b: r is closer to the `mod' function.

This makes

and

simpler to prove, since two quadrants can be easily taken care of on the first induction.

About: