proposition: Theorem eqb_equiv : forall x y, eqb x y = Beqb (Prim2B x) (Prim2B y).
proof: Proof. intros x y. rewrite eqb_spec. unfold Beqb. now rewrite !B2SF_Prim2B. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN