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).
#[deprecated(since = "8.15.0", note = "Use Z_frexp_spec instead.")]
Notation frexp_spec := Z_frexp_spec (only parsing).

Theorem Z_ldexp_spec : forall f e, Prim2SF (Z.ldexp f e) = SFldexp prec emax (Prim2SF f) e.
#[deprecated(since = "8.15.0", note = "Use Z_ldexp_spec instead.")]
Notation ldexp_spec := Z_ldexp_spec (only parsing).