proposition: Theorem div_equiv : forall x y, Prim2B (x / y) = Bdiv mode_NE (Prim2B x) (Prim2B y).
proof: Proof. intros x y. apply B2Prim_inj. rewrite B2Prim_Prim2B. apply Prim2SF_inj. rewrite Prim2SF_B2Prim. rewrite div_spec. rewrite <-!B2SF_Prim2B. case (Prim2B x) as [sx|sx| |sx mx ex Bx]; case (Prim2B y) as [sy|sy| |sy my ey By]; [now (trivial || simpl; case Bool.eqb).. | ]. simpl. rewrite B2SF_SF2B. set (melz := SFdiv_core_binary _ _ _ _ _ _). case melz as [[mz ez] lz]. apply binary_round_aux_equiv. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN