proposition: Theorem inbetween_int_ZR : forall x m l, inbetween_int m x l -> Ztrunc x = cond_incr (round_ZR (Zlt_bool m 0) l) m.
proof: Proof. Proof with auto with typeclass_instances. intros x m l Hl. inversion_clear Hl as [Hx|l' Hx Hl']. rewrite Hx. rewrite Zrnd_IZR... unfold Ztrunc. assert (Hm: Zfloor x = m). apply Zfloor_imp. exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)). rewrite Zceil_floor_neq. rewrite Hm. unfold cond_incr. simpl. case Rlt_bool_spec ; intros Hx' ; case Zlt_bool_spec ; intros Hm' ; try apply refl_equal. elim Rlt_not_le with (1 := Hx'). apply Rlt_le. apply Rle_lt_trans with (2 := proj1 Hx). now apply IZR_le. elim Rle_not_lt with (1 := Hx'). apply Rlt_le_trans with (1 := proj2 Hx). apply IZR_le. now apply Zlt_le_succ. rewrite Hm. now apply Rlt_not_eq. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket