proposition: Theorem round_odd_opp : forall x, round beta fexp Zrnd_odd (-x) = (- round beta fexp Zrnd_odd x)%R.
proof: Proof. intros x; unfold round. rewrite <- F2R_Zopp. unfold F2R; simpl. apply f_equal2; apply f_equal. rewrite scaled_mantissa_opp. generalize (scaled_mantissa beta fexp x); intros r. unfold Zrnd_odd. case (Req_EM_T (- r) (IZR (Zfloor (- r)))). case (Req_EM_T r (IZR (Zfloor r))). intros Y1 Y2. apply eq_IZR. now rewrite opp_IZR, <- Y1, <-Y2. intros Y1 Y2. absurd (r=IZR (Zfloor r)); trivial. pattern r at 2; replace r with (-(-r))%R by ring. rewrite Y2, <- opp_IZR. rewrite Zfloor_IZR. rewrite opp_IZR, <- Y2. ring. case (Req_EM_T r (IZR (Zfloor r))). intros Y1 Y2. absurd (-r=IZR (Zfloor (-r)))%R; trivial. pattern r at 2; rewrite Y1. rewrite <- opp_IZR, Zfloor_IZR. now rewrite opp_IZR, <- Y1. intros Y1 Y2. unfold Zceil; rewrite Ropp_involutive. replace (Z.even (Zfloor (- r))) with (negb (Z.even (Zfloor r))). case (Z.even (Zfloor r)); simpl; ring. apply trans_eq with (Z.even (Zceil r)). rewrite Zceil_floor_neq. rewrite Z.even_add. destruct (Z.even (Zfloor r)); reflexivity. now apply sym_not_eq. rewrite <- (Z.even_opp (Zfloor (- r))). reflexivity. apply cexp_opp. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations