proposition: Lemma Prim2B_B2Prim : forall x, Prim2B (B2Prim x) = x.
proof: Proof. intro x. unfold Prim2B, B2Prim. apply B2SF_inj. rewrite B2SF_SF2B. apply Prim2SF_SF2Prim. apply valid_binary_B2SF. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN