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