proposition: Theorem ldexp_equiv : forall x e, Prim2B (Z.ldexp x e) = Bldexp mode_NE (Prim2B x) e.
proof: Proof. intros x e. apply B2Prim_inj. rewrite B2Prim_Prim2B. apply Prim2SF_inj. rewrite Prim2SF_B2Prim. rewrite Z_ldexp_spec. rewrite <-!B2SF_Prim2B. case (Prim2B x) as [sx|sx| |sx mx ex Bx]; [now trivial.. | ]. simpl. rewrite B2SF_SF2B. apply binary_round_equiv. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN