proposition: Lemma of_int63_of_pos_exact p : (p < 2^53)%positive -> toX (of_int63 (Int63.of_pos p)) = Xreal (IZR (Zpos p)).
proof: Proof. intro H. assert (Hp : Int63.to_Z (of_pos p) = Zpos p). { replace (Int63.of_pos p) with (Int63.of_Z (Zpos p)); [ |now simpl]. rewrite of_Z_spec, Zmod_small; [now simpl|split; [now simpl| ]]. now apply (Z.lt_le_trans _ _ _ (Pos2Z.pos_lt_pos _ _ H)); compute. } rewrite of_int63_exact; rewrite Hp; [reflexivity| ]. apply (Z.le_trans _ _ _ (Z.lt_le_incl _ _ (Pos2Z.pos_lt_pos _ _ H))). now compute. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig