proposition: Theorem inbetween_int_NA : forall x m l, inbetween_int m x l -> ZnearestA x = cond_incr (round_N (Zle_bool 0 m) l) m.
proof: Proof. intros x m l Hl. now apply inbetween_int_N with (choice := fun x => Zle_bool 0 x). Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket