proposition: Theorem F2R_eq : forall e m1 m2 : Z, (m1 = m2)%Z -> (F2R (Float beta m1 e) = F2R (Float beta m2 e))%R.
proof: Proof. intros e m1 m2 H. now apply (f_equal (fun m => F2R (Float beta m e))). Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits