proposition: Theorem F2R_Zopp : forall m e : Z, F2R (Float beta (Z.opp m) e) = Ropp (F2R (Float beta m e)).
proof: Proof. intros m e. unfold F2R. simpl. rewrite <- Ropp_mult_distr_l_reverse. now rewrite opp_IZR. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits