proposition: Lemma round_N_le_le_midp : forall choice u v, F u -> (round beta fexp (Znearest choice) v <= u)%R -> (v <= (u + succ u) / 2)%R.
proof: Proof. Proof with auto with typeclass_instances. intros choice u v Hu H2. apply Ropp_le_cancel. apply Rle_trans with (((-u)+pred (-u))/2)%R. rewrite pred_opp; right; field. apply round_N_ge_ge_midp with (choice := fun t:Z => negb (choice (- (t + 1))%Z))... apply generic_format_opp... rewrite <- (Ropp_involutive (round _ _ _ _)). rewrite <- round_N_opp, Ropp_involutive. apply Ropp_le_contravar; easy. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop