proposition: Theorem B2R_inj: forall x y : binary_float, is_finite_strict x = true -> is_finite_strict y = true -> B2R x = B2R y -> x = y.
proof: Proof. intros [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy. simpl. intros _ _ Heq. assert (Hs: sx = sy). revert Heq. clear. case sx ; case sy ; try easy ; intros Heq ; apply False_ind ; revert Heq. apply Rlt_not_eq. apply Rlt_trans with R0. now apply F2R_lt_0. now apply F2R_gt_0. apply Rgt_not_eq. apply Rgt_trans with R0. now apply F2R_gt_0. now apply F2R_lt_0. assert (mx = my /\ ex = ey). refine (_ (canonical_unique _ fexp _ _ _ _ Heq)). rewrite Hs. now case sy ; intro H ; injection H ; split. now apply canonical_bounded. now apply canonical_bounded. revert Hx. rewrite Hs, (proj1 H), (proj2 H). intros Hx. apply f_equal. apply eqbool_irrelevance. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative