proposition: Theorem Rnd_NA_pt_N : forall F : R -> Prop, F 0 -> forall x f : R, Rnd_N_pt F x f -> (Rabs x <= Rabs f)%R -> Rnd_NA_pt F x f.
proof: Proof. intros F HF x f Rxf Hxf. split. apply Rxf. intros g Rxg. destruct (Rabs_eq_Rabs (f - x) (g - x)) as [H|H]. apply Rle_antisym. apply Rxf. apply Rxg. apply Rxg. apply Rxf. replace g with f. apply Rle_refl. apply Rplus_eq_reg_r with (1 := H). assert (g = 2 * x - f)%R. replace (2 * x - f)%R with (x - (f - x))%R by ring. rewrite H. ring. destruct (Rle_lt_dec 0 x) as [Hx|Hx]. revert Hxf. rewrite Rabs_pos_eq with (1 := Hx). rewrite 2!Rabs_pos_eq ; try ( apply (Rnd_N_pt_ge_0 F HF x) ; assumption ). intros Hxf. rewrite H0. apply Rplus_le_reg_r with f. ring_simplify. apply Rmult_le_compat_l with (2 := Hxf). now apply IZR_le. revert Hxf. apply Rlt_le in Hx. rewrite Rabs_left1 with (1 := Hx). rewrite 2!Rabs_left1 ; try ( apply (Rnd_N_pt_le_0 F HF x) ; assumption ). intros Hxf. rewrite H0. apply Ropp_le_contravar. apply Rplus_le_reg_r with f. ring_simplify. apply Rmult_le_compat_l. now apply IZR_le. now apply Ropp_le_cancel. Qed.
imports: Coq(Reals) Raux Defs