proposition: Theorem Rnd_NA_NG_pt : forall F : R -> Prop, F 0 -> forall x f, Rnd_NA_pt F x f <-> Rnd_NG_pt F (fun x f => Rabs x <= Rabs f) x f.
proof: Proof. intros F HF x f. destruct (Rle_or_lt 0 x) as [Hx|Hx]. split ; intros (H1, H2). assert (Hf := Rnd_N_pt_ge_0 F HF x f Hx H1). split. exact H1. destruct (Rnd_N_pt_DN_or_UP _ _ _ H1) as [H3|H3]. right. intros f2 Hxf2. specialize (H2 _ Hxf2). destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H4|H4]. eapply Rnd_DN_pt_unique ; eassumption. apply Rle_antisym. rewrite Rabs_pos_eq with (1 := Hf) in H2. rewrite Rabs_pos_eq in H2. exact H2. now apply Rnd_N_pt_ge_0 with F x. apply Rle_trans with x. apply H3. apply H4. left. rewrite Rabs_pos_eq with (1 := Hf). rewrite Rabs_pos_eq with (1 := Hx). apply H3. split. exact H1. intros f2 Hxf2. destruct H2 as [H2|H2]. assert (Hf := Rnd_N_pt_ge_0 F HF x f Hx H1). assert (Hf2 := Rnd_N_pt_ge_0 F HF x f2 Hx Hxf2). rewrite 2!Rabs_pos_eq ; trivial. rewrite 2!Rabs_pos_eq in H2 ; trivial. destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H3|H3]. apply Rle_trans with (2 := H2). apply H3. apply H3. apply H1. apply H2. rewrite (H2 _ Hxf2). apply Rle_refl. assert (Hx' := Rlt_le _ _ Hx). clear Hx. rename Hx' into Hx. split ; intros (H1, H2). assert (Hf := Rnd_N_pt_le_0 F HF x f Hx H1). split. exact H1. destruct (Rnd_N_pt_DN_or_UP _ _ _ H1) as [H3|H3]. left. rewrite Rabs_left1 with (1 := Hf). rewrite Rabs_left1 with (1 := Hx). apply Ropp_le_contravar. apply H3. right. intros f2 Hxf2. specialize (H2 _ Hxf2). destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H4|H4]. apply Rle_antisym. apply Rle_trans with x. apply H4. apply H3. rewrite Rabs_left1 with (1 := Hf) in H2. rewrite Rabs_left1 in H2. now apply Ropp_le_cancel. now apply Rnd_N_pt_le_0 with F x. eapply Rnd_UP_pt_unique ; eassumption. split. exact H1. intros f2 Hxf2. destruct H2 as [H2|H2]. assert (Hf := Rnd_N_pt_le_0 F HF x f Hx H1). assert (Hf2 := Rnd_N_pt_le_0 F HF x f2 Hx Hxf2). rewrite 2!Rabs_left1 ; trivial. rewrite 2!Rabs_left1 in H2 ; trivial. apply Ropp_le_contravar. apply Ropp_le_cancel in H2. destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H3|H3]. apply H3. apply H1. apply H2. apply Rle_trans with (1 := H2). apply H3. rewrite (H2 _ Hxf2). apply Rle_refl. Qed.
imports: Coq(Reals) Raux Defs