proposition: Theorem B2FF_inj : forall x y : binary_float, B2FF x = B2FF y -> x = y.
proof: Proof. intros [sx|sx|sx plx Hplx|sx mx ex Hx] [sy|sy|sy ply Hply|sy my ey Hy] ; try easy. intros H. now inversion H. intros H. now inversion H. intros H. inversion H. clear H. revert Hplx. rewrite H2. intros Hx. apply f_equal, eqbool_irrelevance. intros H. inversion H. clear H. revert Hx. rewrite H2, H3. intros Hx. apply f_equal, eqbool_irrelevance. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN