proposition: Lemma Z_ldexp_spec f e : Prim2SF (Z.ldexp f e) = SFldexp prec emax (Prim2SF f) e.
proof: Proof. try exact (Z_ldexp_spec f e); exact (ldexp_spec f e). Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN