proposition: Theorem Bulp_correct : forall x, is_finite x = true -> B2R (Bulp x) = ulp radix2 fexp (B2R x) /\ is_finite (Bulp x) = true /\ Bsign (Bulp x) = false.
proof: Proof. intros x Fx. rewrite <- is_finite_B2BSN in Fx. generalize (Bulp_correct prec emax _ _ _ Fx). replace (BinarySingleNaN.Bulp (B2BSN x)) with (B2BSN (Bulp x)) by apply B2BSN_lift. rewrite 2!B2R_B2BSN. now destruct Bulp. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN