proposition: Lemma B2R_BtoX : forall x, is_finite x = true -> BtoX x = Xreal (B2R x).
proof: Proof. intros [s|s| |s m e B] ; try easy. intros _. simpl. now rewrite FtoR_split. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig