proposition: Lemma B2Prim_inj : forall x y, B2Prim x = B2Prim y -> x = y.
proof: Proof. intros x y Heq. generalize (f_equal Prim2B Heq). now rewrite 2!Prim2B_B2Prim. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN