fact: Definition mag x := let (_, e) := PrimFloat.frshiftexp x in (Int63.to_Z e - FloatOps.shift)%Z.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig