proposition: Theorem leb_equiv : forall x y, leb x y = Bleb (Prim2B x) (Prim2B y).
proof: Proof. intros x y. rewrite leb_spec. unfold Bleb. now rewrite !B2SF_Prim2B. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN