proposition: Lemma ZtoS_correct: forall prec z, (z <= StoZ (ZtoS z))%Z \/ toX (pow2_UP prec (ZtoS z)) = Xnan.
proof: Proof. now left. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig