proposition: Lemma toX_Prim2B x : toX x = BtoX (Prim2B x).
proof: Proof. now unfold toX, toF; rewrite <-B2SF_Prim2B; case Prim2B. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig