proposition: Theorem is_finite_equiv : forall x, PrimFloat.is_finite x = is_finite (Prim2B x).
proof: Proof. intro x. unfold PrimFloat.is_finite. rewrite is_nan_equiv, is_infinity_equiv. now case (Prim2B x) as [sx|sx| |sx mx ex Bx]. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN