proposition: Lemma fromZ_correct : forall n, (Z.abs n <= 256)%Z -> toX (fromZ n) = Xreal (IZR n).
proof: Proof. intros [ |p|p] Hp; unfold fromZ; [now simpl| | ]. { case Pos.compare_spec; intro Hp'. { now revert Hp; rewrite Hp'. } { now rewrite (of_int63_of_pos_exact _ Hp'). } lia. } case Pos.compare_spec; intro Hp'. { now revert Hp; rewrite Hp'. } { change (Xreal _) with (- (Xreal (IZR (Zpos p))))%XR. now rewrite <-(of_int63_of_pos_exact _ Hp'), toX_neg. } lia. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig