Proof

We plan here to prove that fdiv in this code or (car (gfdivr 8 (= 0 1))) in this is always correct, rounding included, for positive normal operands whose quotient is normal. We maintain parameters M and z in the Scheme code.

Several theorems are needed. First we need upper bounds for r, the remainder, at each stage and for each range of dividend. This Scheme code computes those limits and this text explains how.