proposition: Theorem Znearest_opp : forall choice x, Znearest choice (- x) = (- Znearest (fun t => negb (choice (- (t + 1))%Z)) x)%Z.
proof: Proof. Proof with auto with typeclass_instances. intros choice x. destruct (Req_dec (IZR (Zfloor x)) x) as [Hx|Hx]. rewrite <- Hx. rewrite <- opp_IZR. rewrite 2!Zrnd_IZR... unfold Znearest. replace (- x - IZR (Zfloor (-x)))%R with (IZR (Zceil x) - x)%R. rewrite Rcompare_ceil_floor_middle with (1 := Hx). rewrite Rcompare_floor_ceil_middle with (1 := Hx). rewrite Rcompare_sym. rewrite <- Zceil_floor_neq with (1 := Hx). unfold Zceil. rewrite Ropp_involutive. case Rcompare ; simpl ; trivial. rewrite Z.opp_involutive. case (choice (Zfloor (- x))) ; simpl ; trivial. now rewrite Z.opp_involutive. now rewrite Z.opp_involutive. unfold Zceil. rewrite opp_IZR. apply Rplus_comm. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop