proposition: Theorem inbetween_int_UP_sign : forall x m l, inbetween_int m (Rabs x) l -> Zceil x = cond_Zopp (Rlt_bool x 0) (cond_incr (round_sign_UP (Rlt_bool x 0) l) m).
proof: Proof. intros x m l Hl. unfold Rabs in Hl. destruct (Rcase_abs x) as [Zx|Zx] . rewrite Rlt_bool_true with (1 := Zx). simpl. unfold Zceil. apply f_equal. inversion_clear Hl ; simpl. rewrite H. apply Zfloor_IZR. apply Zfloor_imp. split. now apply Rlt_le. apply H. rewrite Rlt_bool_false. simpl. inversion_clear Hl ; simpl. rewrite H. apply Zceil_IZR. apply Zceil_imp. split. change (m + 1 - 1)%Z with (Z.pred (Z.succ m)). now rewrite <- Zpred_succ. now apply Rlt_le. now apply Rge_le. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket