proposition: Theorem compare_equiv : forall x y, (x ?= y)%float = flatten_cmp_opt (Bcompare (Prim2B x) (Prim2B y)).
proof: Proof. intros x y. rewrite compare_spec. rewrite <-!B2SF_Prim2B. now case (Prim2B x) as [sx|sx| |sx mx ex Bx]; case (Prim2B y) as [sy|sy| |sy my ey By]. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN