proposition: Theorem mul_equiv : forall x y, Prim2B (x * y) = Bmult mode_NE (Prim2B x) (Prim2B y).
proof: Proof. intros x y. apply B2Prim_inj. rewrite B2Prim_Prim2B. apply Prim2SF_inj. rewrite Prim2SF_B2Prim. rewrite mul_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. rewrite B2SF_SF2B. apply binary_round_aux_equiv. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN