Correctness of division backends

word_eq_spec identifies the complete dispatcher with Spec.div for every descriptor and operand pair. The equality includes rounding, signed zeros, infinities, and NaNs.

The specialized kernels provide refinements on their accepted inputs. When an operand or intermediate lies outside a kernel's supported domain, the dispatcher uses generic, whose correctness is established by generic_eq_spec. Runtime clients can import Div.Runtime separately.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.DivBackend.generic_eq_spec {fmt : FloatFormat} (x y : Model fmt) : generic x y = Spec.div x y

Compact generic division preserves the public exact-dyadic operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.DivBackend.word_eq_spec {fmt : FloatFormat} (x y : Model fmt) : word x y = Spec.div x y

Structurally selected specialized dispatch preserves format-generic division.