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