proposition: Lemma B2SF_Prim2B : forall x, B2SF (Prim2B x) = Prim2SF x.
proof: Proof. intros x. apply SF2Prim_inj. - rewrite SF2Prim_Prim2SF. apply B2Prim_Prim2B. - apply valid_binary_B2SF. - apply Prim2SF_valid. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN