proposition: Theorem is_zero_equiv : forall x, is_zero x = match Prim2B x with B754_zero _ => true | _ => false end.
proof: Proof. intro x. unfold is_zero. rewrite eqb_spec. rewrite <-B2SF_Prim2B. now case Prim2B as [sx|sx| |sx mx ex Bx]; try reflexivity; case sx. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN