proposition: Lemma round_N_eq_ties: forall c1 c2 x, (x - round beta fexp Zfloor x <> round beta fexp Zceil x - x)%R -> (round beta fexp (Znearest c1) x = round beta fexp (Znearest c2) x)%R.
proof: Proof. Proof with auto with typeclass_instances. intros c1 c2 x. pose (d:=round beta fexp Zfloor x); pose (u:=round beta fexp Zceil x); fold d; fold u; intros H. case (Rle_or_lt ((d+u)/2) x); intros L. 2:rewrite 2!round_N_eq_DN... destruct L as [L|L]. rewrite 2!round_N_eq_UP... contradict H; rewrite <- L; field. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop