proposition: Theorem round_N_odd : forall x, round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) = round beta fexp (Znearest choice) x.
proof: Proof. Proof with auto with typeclass_instances. intros x. case (total_order_T x 0); intros H; [case H; clear H; intros H | idtac]. rewrite <- (Ropp_involutive x). rewrite round_odd_opp. rewrite 2!round_N_opp. apply f_equal. destruct (canonical_generic_format beta fexp (round beta fexp Zfloor (-x))) as (d,(Hd1,Hd2)). apply generic_format_round... destruct (canonical_generic_format beta fexp (round beta fexp Zceil (-x))) as (u,(Hu1,Hu2)). apply generic_format_round... apply round_N_odd_pos with d u... rewrite <- Hd1; apply round_DN_pt... rewrite <- Hu1; apply round_UP_pt... auto with real. rewrite H; repeat rewrite round_0... destruct (canonical_generic_format beta fexp (round beta fexp Zfloor x)) as (d,(Hd1,Hd2)). apply generic_format_round... destruct (canonical_generic_format beta fexp (round beta fexp Zceil x)) as (u,(Hu1,Hu2)). apply generic_format_round... apply round_N_odd_pos with d u... rewrite <- Hd1; apply round_DN_pt... rewrite <- Hu1; apply round_UP_pt... Qed.
imports: Coq(ZArith Reals Psatz) Core Operations