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

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.