Verified native normal-result division for binary64

The native path generates quotient bits with a restoring UInt64 loop. Every accepted result equals the exact-rational finite result as an encoded value. divFiniteFastImpl_eq extends this agreement to the complete optional finite operation, including declined inputs.

Zeros and quotients outside the normal-result path use the generic finite kernel. Non-finite operands remain the responsibility of the outer arithmetic dispatcher.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.divFiniteFastImpl_eq (x y : Value) : divFiniteFastImpl? x y = divFiniteImpl? x y

The native candidate plus certified general route equals the existing finite binary64 implementation.