proposition: Theorem ltb_equiv : forall x y, ltb x y = Bltb (Prim2B x) (Prim2B y).
proof: Proof. intros x y. rewrite ltb_spec. unfold Bltb. now rewrite !B2SF_Prim2B. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN