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 frexp_spec : forall f, let (m,e) := frexp f in (Prim2SF m , e ) = SFfrexp prec emax (Prim2SF f).

Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2SF f) e.