proposition: Theorem opp_equiv : forall x, Prim2B (- x) = Bopp (Prim2B x).
proof: Proof. intro x. apply B2Prim_inj. rewrite B2Prim_Prim2B. apply Prim2SF_inj. rewrite Prim2SF_B2Prim. rewrite opp_spec. rewrite <-B2SF_Prim2B. now case Prim2B as [sx|sx| |sx mx ex Bx]. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN