proposition: Theorem F2R_cond_Zopp : forall b m e, F2R (Float beta (cond_Zopp b m) e) = cond_Ropp b (F2R (Float beta m e)).
proof: Proof. intros [|] m e ; unfold F2R ; simpl. now rewrite opp_IZR, Ropp_mult_distr_l_reverse. apply refl_equal. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits