proposition: Theorem round_N_le_midp: forall choice u v, F u -> (v < (u + succ u)/2)%R -> (round beta fexp (Znearest choice) v <= u)%R.
proof: Proof. Proof with auto with typeclass_instances. intros choice u v Fu H. assert (V: ((succ u = 0 /\ u = 0) \/ u < succ u)%R). specialize (succ_ge_id u); intros P; destruct P as [P|P]. now right. case (Req_dec u 0); intros Zu. left; split; trivial. now rewrite <- P. right; now apply succ_gt_id. destruct V as [(V1,V2)|V]. rewrite V2; apply round_le_generic... apply generic_format_0. left; apply Rlt_le_trans with (1:=H). rewrite V1,V2; right; field. assert (T: (u < (u + succ u) / 2 < succ u)%R) by lra. destruct T as (T1,T2). apply Rnd_N_pt_monotone with F v ((u + succ u) / 2)%R... apply round_N_pt... apply Rnd_N_pt_DN with (succ u)%R. pattern u at 3; replace u with (round beta fexp Zfloor ((u + succ u) / 2)). apply round_DN_pt... apply round_DN_eq; trivial. split; try left; assumption. pattern (succ u) at 2; replace (succ u) with (round beta fexp Zceil ((u + succ u) / 2)). apply round_UP_pt... apply round_UP_eq; trivial. apply generic_format_succ... rewrite pred_succ; trivial. split; try left; assumption. right; field. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop