proposition: Lemma Prim2SF_B2Prim : forall x, Prim2SF (B2Prim x) = B2SF x.
proof: Proof. intro x; unfold B2Prim. now rewrite Prim2SF_SF2Prim; [ | apply valid_binary_B2SF]. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN