proposition: Theorem split_bits_inj : forall x y, (0 <= x < Zpower 2 (mw + ew + 1))%Z -> (0 <= y < Zpower 2 (mw + ew + 1))%Z -> split_bits x = split_bits y -> x = y.
proof: Proof. intros x y Hx Hy. generalize (join_split_bits x Hx) (join_split_bits y Hy). destruct (split_bits x) as ((sx, mx), ex). destruct (split_bits y) as ((sy, my), ey). intros Jx Jy H. revert Jx Jy. inversion_clear H. intros Jx Jy. now rewrite <- Jx. Qed.
imports: Coq(ZArith Reals Lia SpecFloat) Core BinarySingleNaN Binary