proposition: Theorem B2SF_inj : forall x y : binary_float, B2SF x = B2SF y -> x = y.
proof: Proof. intros [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy. intros H. now inversion H. intros H. now inversion H. 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