proposition: Theorem round_val_of_pred : forall rnd : R -> R -> Prop, round_pred rnd -> forall x, { f : R | rnd x f }.
proof: Proof. intros rnd (H1,H2) x. specialize (H1 x). assert (H3 : bound (rnd x)). destruct H1 as (f, H1). exists f. intros g Hg. now apply H2 with (3 := Rle_refl x). exists (proj1_sig (completeness _ H3 H1)). destruct completeness as (f1, (H4, H5)). simpl. destruct H1 as (f2, H1). assert (f1 = f2). apply Rle_antisym. apply H5. intros f3 H. now apply H2 with (3 := Rle_refl x). now apply H4. now rewrite H. Qed.
imports: Coq(Reals) Raux Defs