proposition: Theorem ulp_equiv : forall x, Prim2B (ulp x) = Bulp' (Prim2B x).
proof: Proof. intro x. unfold ulp, Bulp'. rewrite one_equiv, ldexp_equiv, Prim2B_B2Prim. generalize (frexp_equiv x). case Z.frexp; intros f e. destruct Bfrexp as [f' e']. now intros [= _ <-]. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN