IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The q and r computed by the extracts of these theorems are not the same as those returned by the divides(a;b) and remainder(a;b) built-in arithmetic functions:
with those functions, the sign of r follows the sign of a and div has simple symmetry properties. 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 the gcd_exists and bezout_ident_ theorems simpler to prove, since two quadrants can be easily taken care of on the first induction.
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html