proposition: Lemma B2Prim_Prim2B : forall x, B2Prim (Prim2B x) = x.
proof: Proof. intros x. unfold Prim2B, B2Prim. now rewrite B2SF_SF2B, SF2Prim_Prim2SF. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN