proposition: Theorem satisfies_any_imp_ZR : forall F : R -> Prop, satisfies_any F -> round_pred (Rnd_ZR_pt F).
proof: Proof. intros F Hany. split. intros x. destruct (Rle_or_lt 0 x) as [Hx|Hx]. destruct (proj1 (satisfies_any_imp_DN F Hany) x) as (f, Hf). exists f. split. now intros _. intros Hx'. assert (x = 0). now apply Rle_antisym. rewrite H in Hf |- *. clear H Hx Hx'. rewrite Rnd_DN_pt_idempotent with (1 := Hf). apply Rnd_UP_pt_refl. apply Hany. apply Hany. destruct (proj1 (satisfies_any_imp_UP F Hany) x) as (f, Hf). exists f. split. intros Hx'. elim (Rlt_irrefl 0). now apply Rle_lt_trans with x. now intros _. apply Rnd_ZR_pt_monotone. apply Hany. Qed.
imports: Coq(Reals) Raux Defs