proposition: Theorem fromZ_small_correct : forall v, (Z.abs v <= 256)%Z -> contains (convert (fromZ_small v)) (Xreal (IZR v)).
proof: Proof. intros. simpl. rewrite F'.valid_lb_real, F'.valid_ub_real by now rewrite F.real_correct, F.fromZ_correct. rewrite F.fromZ_correct by easy. split ; apply Rle_refl. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval