proposition: Theorem round_fun_of_pred : forall rnd : R -> R -> Prop, round_pred rnd -> { f : R -> R | forall x, rnd x (f x) }.
proof: Proof. intros rnd H. exists (fun x => proj1_sig (round_val_of_pred rnd H x)). intros x. now destruct round_val_of_pred as (f, H1). Qed.
imports: Coq(Reals) Raux Defs