proposition: Theorem satisfies_any_imp_NG : forall (F : R -> Prop) (P : R -> R -> Prop), satisfies_any F -> NG_existence_prop F P -> round_pred_total (Rnd_NG_pt F P).
proof: Proof. intros F P Hany HP x. destruct (proj1 (satisfies_any_imp_DN F Hany) x) as (d, Hd). destruct (proj1 (satisfies_any_imp_UP F Hany) x) as (u, Hu). destruct (total_order_T (Rabs (u - x)) (Rabs (d - x))) as [[H|H]|H]. exists u. split. split. apply Hu. intros g Hg. destruct (Rle_or_lt x g) as [Hxg|Hxg]. rewrite 2!Rabs_pos_eq. apply Rplus_le_compat_r. now apply Hu. now apply Rle_0_minus. apply Rle_0_minus. apply Hu. apply Rlt_le in Hxg. apply Rlt_le. apply Rlt_le_trans with (1 := H). do 2 rewrite <- (Rabs_minus_sym x). rewrite 2!Rabs_pos_eq. apply Rplus_le_compat_l. apply Ropp_le_contravar. now apply Hd. now apply Rle_0_minus. apply Rle_0_minus. apply Hd. right. intros f Hf. destruct (Rnd_N_pt_DN_or_UP_eq F x _ _ _ Hd Hu Hf) as [K|K] ; rewrite K. elim Rlt_not_le with (1 := H). rewrite <- K. apply Hf. apply Hu. apply refl_equal. destruct (Req_dec x d) as [He|Hne]. exists x. split. apply Rnd_N_pt_refl. rewrite He. apply Hd. right. intros. apply Rnd_N_pt_idempotent with (1 := H0). rewrite He. apply Hd. assert (Hf : ~F x). intros Hf. apply Hne. apply sym_eq. now apply Rnd_DN_pt_idempotent with (1 := Hd). destruct (HP x _ _ Hf Hd Hu) as [H'|H']. exists u. split. split. apply Hu. intros g Hg. destruct (Rle_or_lt x g) as [Hxg|Hxg]. rewrite 2!Rabs_pos_eq. apply Rplus_le_compat_r. now apply Hu. now apply Rle_0_minus. apply Rle_0_minus. apply Hu. apply Rlt_le in Hxg. rewrite H. rewrite 2!Rabs_left1. apply Ropp_le_contravar. apply Rplus_le_compat_r. now apply Hd. now apply Rle_minus. apply Rle_minus. apply Hd. now left. exists d. split. split. apply Hd. intros g Hg. destruct (Rle_or_lt x g) as [Hxg|Hxg]. rewrite <- H. rewrite 2!Rabs_pos_eq. apply Rplus_le_compat_r. now apply Hu. now apply Rle_0_minus. apply Rle_0_minus. apply Hu. apply Rlt_le in Hxg. rewrite 2!Rabs_left1. apply Ropp_le_contravar. apply Rplus_le_compat_r. now apply Hd. now apply Rle_minus. apply Rle_minus. apply Hd. now left. exists d. split. split. apply Hd. intros g Hg. destruct (Rle_or_lt x g) as [Hxg|Hxg]. apply Rlt_le. apply Rlt_le_trans with (1 := H). rewrite 2!Rabs_pos_eq. apply Rplus_le_compat_r. now apply Hu. now apply Rle_0_minus. apply Rle_0_minus. apply Hu. apply Rlt_le in Hxg. rewrite 2!Rabs_left1. apply Ropp_le_contravar. apply Rplus_le_compat_r. now apply Hd. now apply Rle_minus. apply Rle_minus. apply Hd. right. intros f Hf. destruct (Rnd_N_pt_DN_or_UP_eq F x _ _ _ Hd Hu Hf) as [K|K] ; rewrite K. apply refl_equal. elim Rlt_not_le with (1 := H). rewrite <- K. apply Hf. apply Hd. Qed.
imports: Coq(Reals) Raux Defs