proposition: Theorem satisfies_any_imp_UP : forall F : R -> Prop, satisfies_any F -> round_pred (Rnd_UP_pt F).
proof: Proof. intros F Hany. split. intros x. destruct (proj1 (satisfies_any_imp_DN F Hany) (-x)) as (f, Hf). exists (-f). rewrite <- (Ropp_involutive x). apply Rnd_UP_pt_opp. apply Hany. exact Hf. apply Rnd_UP_pt_monotone. Qed.
imports: Coq(Reals) Raux Defs