proposition: Theorem inbetween_int_N : forall choice x m l, inbetween_int m x l -> Znearest choice x = cond_incr (round_N (choice m) l) m.
proof: Proof. Proof with auto with typeclass_instances. intros choice x m l Hl. inversion_clear Hl as [Hx|l' Hx Hl']. rewrite Hx. rewrite Zrnd_IZR... unfold Znearest. assert (Hm: Zfloor x = m). apply Zfloor_imp. exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)). rewrite Zceil_floor_neq. rewrite Hm. replace (Rcompare (x - IZR m) (/2)) with l'. now case l'. rewrite <- Hl'. rewrite plus_IZR. rewrite <- (Rcompare_plus_r (- IZR m) x). apply f_equal. field. rewrite Hm. now apply Rlt_not_eq. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket