proposition: Theorem inbetween_int_ZR_sign : forall x m l, inbetween_int m (Rabs x) l -> Ztrunc x = cond_Zopp (Rlt_bool x 0) m.
proof: Proof. intros x m l Hl. simpl. unfold Ztrunc. destruct (Rlt_le_dec x 0) as [Zx|Zx]. rewrite Rlt_bool_true with (1 := Zx). simpl. unfold Zceil. apply f_equal. apply Zfloor_imp. rewrite <- Rabs_left with (1 := Zx). apply inbetween_bounds with (2 := Hl). apply IZR_lt. apply Zlt_succ. rewrite Rlt_bool_false with (1 := Zx). simpl. apply Zfloor_imp. rewrite <- Rabs_pos_eq with (1 := Zx). apply inbetween_bounds with (2 := Hl). apply IZR_lt. apply Zlt_succ. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket