Verified native normal-result division for binary64

The native path generates quotient bits with a restoring UInt64 loop. Every accepted result equals the generic finite kernel's result, and divFinite_eq_divFiniteComponents extends this agreement to the whole optional finite operation, declined inputs included.

Zeros and quotients outside the normal-result path use the generic finite kernel. Non-finite operands are handled by the outer arithmetic dispatcher.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.NativeBinary64.divFinite_eq_divFiniteComponents (x y : Value) : divFinite? x y = divFiniteComponents? x y

Native finite division with its fallback equals the generic component kernel.