proposition: Theorem inbetween_int_NE_sign : forall x m l, inbetween_int m (Rabs x) l -> ZnearestE x = cond_Zopp (Rlt_bool x 0) (cond_incr (round_N (negb (Z.even m)) l) m).
proof: Proof. intros x m l Hl. erewrite inbetween_int_N_sign with (choice := fun x => negb (Z.even x)). 2: eexact Hl. apply f_equal. case Rlt_bool. rewrite Z.even_opp, Z.even_add. now case (Z.even m). apply refl_equal. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket