proposition: Theorem inbetween_int_N_sign : forall choice x m l, inbetween_int m (Rabs x) l -> Znearest choice x = cond_Zopp (Rlt_bool x 0) (cond_incr (round_N (if Rlt_bool x 0 then negb (choice (-(m + 1))%Z) else choice m) l) m).
proof: Proof. Proof with auto with typeclass_instances. intros choice x m l Hl. simpl. unfold Rabs in Hl. destruct (Rcase_abs x) as [Zx|Zx]. rewrite Rlt_bool_true with (1 := Zx). simpl. rewrite <- (Ropp_involutive x). rewrite Znearest_opp. apply f_equal. inversion_clear Hl as [Hx|l' Hx Hl']. rewrite Hx. apply Zrnd_IZR... assert (Hm: Zfloor (-x) = m). apply Zfloor_imp. exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)). unfold Znearest. rewrite Zceil_floor_neq. rewrite Hm. replace (Rcompare (- x - IZR m) (/2)) with l'. now case l'. rewrite <- Hl'. rewrite plus_IZR. rewrite <- (Rcompare_plus_r (- IZR m) (-x)). apply f_equal. field. rewrite Hm. now apply Rlt_not_eq. generalize (Rge_le _ _ Zx). clear Zx. intros Zx. rewrite Rlt_bool_false with (1 := Zx). simpl. inversion_clear Hl as [Hx|l' Hx Hl']. rewrite Hx. apply Zrnd_IZR... assert (Hm: Zfloor x = m). apply Zfloor_imp. exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)). unfold Znearest. rewrite Zceil_floor_neq. rewrite Hm. replace (Rcompare (x - IZR m) (/2)) with l'. now case l'. rewrite <- Hl'. rewrite plus_IZR. rewrite <- (Rcompare_plus_r (- IZR m) x). apply f_equal. field. rewrite Hm. now apply Rlt_not_eq. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket