proposition: Theorem inbetween_int_DN_sign : forall x m l, inbetween_int m (Rabs x) l -> Zfloor x = cond_Zopp (Rlt_bool x 0) (cond_incr (round_sign_DN (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). inversion_clear Hl ; simpl. rewrite <- (Ropp_involutive x). rewrite H, <- opp_IZR. apply Zfloor_IZR. apply Zfloor_imp. split. apply Rlt_le. rewrite opp_IZR. apply Ropp_lt_cancel. now rewrite Ropp_involutive. ring_simplify (- (m + 1) + 1)%Z. rewrite opp_IZR. apply Ropp_lt_cancel. now rewrite Ropp_involutive. rewrite Rlt_bool_false. inversion_clear Hl ; simpl. rewrite H. apply Zfloor_IZR. apply Zfloor_imp. split. now apply Rlt_le. apply H. now apply Rge_le. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket