proposition: Theorem satisfies_any_imp_N0 : forall F : R -> Prop, F 0 -> satisfies_any F -> round_pred (Rnd_N0_pt F).
proof: Proof. intros F HF0 Hany. split. assert (H : round_pred_total (Rnd_NG_pt F (fun a b => (Rabs b <= Rabs a)%R))). apply satisfies_any_imp_NG. apply Hany. intros x d u Hf Hd Hu. destruct (Rle_lt_dec 0 x) as [Hx|Hx]. right. rewrite Rabs_pos_eq with (1 := Hx). rewrite Rabs_pos_eq. apply Hd. apply Hd; try easy. left. rewrite Rabs_left with (1 := Hx). rewrite Rabs_left1. apply Ropp_le_contravar. apply Hu. apply Hu; try easy. now apply Rlt_le. intros x. destruct (H x) as (f, Hf). exists f. apply <- Rnd_N0_NG_pt. apply Hf. apply HF0. apply Rnd_N0_pt_monotone. apply HF0. Qed.
imports: Coq(Reals) Raux Defs