The Coq Proof Assistant

# Library Coq.Floats.FloatLemmas

Require Import ZArith Uint63 SpecFloat PrimFloat FloatOps FloatAxioms.
Require Import Psatz.

# Support results involving frexp and ldexp

Lemma shift_value : shift = (2*emax + prec)%Z.
Theorem Z_frexp_spec : forall f, let (m,e) := Z.frexp f in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF f).
Theorem Z_ldexp_spec : forall f e, Prim2SF (Z.ldexp f e) = SFldexp prec emax (Prim2SF f) e.