proposition: Theorem get_sign_equiv : forall x, get_sign x = Bsign (Prim2B x).
proof: Proof. intro x. unfold get_sign. rewrite is_zero_equiv. rewrite ltb_spec. rewrite <-(B2Prim_Prim2B x). case (Prim2B x) as [sx|sx| |sx mx ex Bx]; rewrite Prim2B_B2Prim. - now rewrite div_spec; case sx. - now case sx. - now simpl. - now rewrite Prim2SF_B2Prim; case sx. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN