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