proposition: Theorem eq_F2R : forall e m1 m2 : Z, F2R (Float beta m1 e) = F2R (Float beta m2 e) -> m1 = m2.
proof: Proof. intros e m1 m2 H. apply Zle_antisym ; apply le_F2R with e ; rewrite H ; apply Rle_refl. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits