proposition: Theorem round_N_ge_midp: forall choice u v, F u -> ((u + pred u)/2 < v)%R -> (u <= round beta fexp (Znearest choice) v)%R.
proof: Proof. Proof with auto with typeclass_instances. intros choice u v Fu H. rewrite <- (Ropp_involutive v). rewrite round_N_opp. rewrite <- (Ropp_involutive u). apply Ropp_le_contravar. apply round_N_le_midp. now apply generic_format_opp. apply Ropp_lt_cancel. rewrite Ropp_involutive. apply Rle_lt_trans with (2:=H). unfold pred. right; field. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop