proposition: Theorem is_infinity_equiv : forall x, is_infinity x = match Prim2B x with B754_infinity _ => true | _ => false end.
proof: Proof. intro x. unfold is_infinity. rewrite eqb_spec. rewrite <-B2SF_Prim2B. rewrite B2SF_Prim2B, abs_spec. rewrite <-B2SF_Prim2B. now case Prim2B. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN