Midpoint parity of the delivered remainder

The exact-value identity and half-divisor bound establish the nearest integer quotient. If the returned remainder has half the divisor's magnitude, the quotient in the exact-value identity is even.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainder_magnitude (f : Format) (sx sy : Bool) (cx cy : ℕ) (qx qy : ℤ) (hc : cy ≠ 0) (v : ℚ) (hv : (remainder f (Datum.finite sx cx qx) (Datum.finite sy cy qy)).value.toRat? = some v) : |v| = ↑(remainderCoefficient (cx * 10 ^ (qx - min qx qy).toNat) (cy * 10 ^ (qy - min qx qy).toNat)) * 10 ^ min qx qy

The delivered magnitude is the unrounded integer residual on the common grid.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.remainder_even_at_midpoint (f : Format) (sx sy : Bool) (cx cy : ℕ) (qx qy : ℤ) (hc : cy ≠ 0) (v : ℚ) (hv : (remainder f (Datum.finite sx cx qx) (Datum.finite sy cy qy)).value.toRat? = some v) (htie : 2 * |v| = ↑cy * 10 ^ qy) : remainderInteger sx sy cx cy qx qy % 2 = 0

If the delivered remainder has exactly half the divisor's magnitude, its quotient is even.