proposition: Theorem inbetween_int_NA_sign : forall x m l, inbetween_int m (Rabs x) l -> ZnearestA x = cond_Zopp (Rlt_bool x 0) (cond_incr (round_N true l) m).
proof: Proof. intros x m l Hl. erewrite inbetween_int_N_sign with (choice := Zle_bool 0). 2: eexact Hl. apply f_equal. assert (Hm: (0 <= m)%Z). apply Zlt_succ_le. apply lt_IZR. apply Rle_lt_trans with (Rabs x). apply Rabs_pos. refine (proj2 (inbetween_bounds _ _ _ _ _ Hl)). apply IZR_lt. apply Zlt_succ. rewrite Zle_bool_true with (1 := Hm). rewrite Zle_bool_false. now case Rlt_bool. lia. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket