proposition: Lemma fromZ_correct : forall n, (Z.abs n <= 256)%Z -> toX (fromZ n) = Xreal (IZR n).
proof: Proof. intros n _. apply fromZ_correct'. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig