proposition: Lemma round_N_ge_ge_midp : forall choice u v, F u -> (u <= round beta fexp (Znearest choice) v)%R -> ((u + pred u) / 2 <= v)%R.
proof: Proof. Proof with auto with typeclass_instances. intros choice u v Hu H2. assert (K: ((u=0)%R /\ negligible_exp = None) \/ (pred u < u)%R). case (Req_dec u 0); intros Zu. case_eq (negligible_exp). intros n Hn; right. rewrite Zu, pred_0. unfold ulp; rewrite Req_bool_true, Hn; try easy. rewrite <- Ropp_0. apply Ropp_lt_contravar, bpow_gt_0. intros _; left; split; easy. right. apply pred_lt_id... case K. intros (K1,K2). rewrite K1, pred_0. unfold ulp; rewrite Req_bool_true, K2; try easy. replace ((0+-0)/2)%R with 0%R by field. case (Rle_or_lt 0 v); try easy. intros H3; contradict H2. rewrite K1; apply Rlt_not_le. assert (H4: (round beta fexp (Znearest choice) v <= 0)%R). apply round_le_generic... apply generic_format_0... now left. case H4; try easy. intros H5. absurd (v=0)%R; try auto with real. apply eq_0_round_0_negligible_exp with (Znearest choice)... intros K1. case (Rle_or_lt ((u + pred u) / 2) v); try easy. intros H3. absurd (u <= round beta fexp (Znearest choice) v)%R; try easy. apply Rlt_not_le. apply Rle_lt_trans with (2:=K1). apply round_N_le_midp... apply generic_format_pred... rewrite succ_pred... apply Rlt_le_trans with (1:=H3). right; f_equal; ring. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop