Correctness of native-word division for binary32

These proofs connect the native logarithm, quotient rounding and finite divider to the generic exact-rational specification. Runtime clients can import Division.Runtime without them.

For significands below 2^24 the scaling shifts and rounded quotient fit in UInt64, and those bounds connect native quotient-and-remainder rounding to exact rational rounding, with ties, subnormal results and overflow included.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.roundRatScaledWord_eq (sign : Bool) (num den : UInt64) (exponent : ℤ) (hnumFit : num.toNat < 2 ^ 24) (hdenFit : den.toNat < 2 ^ 24) : roundRatScaledWord sign num den exponent = roundRatScaled sign num.toNat den.toNat exponent

Native-word rational rounding agrees with the exact binary32 rounder roundRatScaled.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary32.divFiniteWord_eq (x y : Value) : divFiniteWord? x y = divFinite? x y

One-word finite division equals the exact-rational divFinite?.