proposition: Theorem inbetween_float_NE : forall x m l, let e := cexp beta fexp x in inbetween_float beta m e x l -> round beta fexp ZnearestE x = F2R (Float beta (cond_incr (round_N (negb (Z.even m)) l) m) e).
proof: Proof. apply inbetween_float_round with (choice := fun m l => cond_incr (round_N (negb (Z.even m)) l) m). exact inbetween_int_NE. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket