proposition: Lemma Rnd_NA_pt_unique_prop : forall F : R -> Prop, F 0 -> Rnd_NG_pt_unique_prop F (fun a b => (Rabs a <= Rabs b)%R).
proof: Proof. intros F HF x d u Hxd1 Hxd2 Hxu1 Hxu2 Hd Hu. apply Rle_antisym. apply Rle_trans with x. apply Hxd1. apply Hxu1. destruct (Rle_or_lt 0 x) as [Hx|Hx]. apply Hxu1. apply Hxd1. rewrite Rabs_pos_eq with (1 := Hx) in Hd. rewrite Rabs_pos_eq in Hd. exact Hd. now apply Hxd1. apply Hxd1. apply Hxu1. rewrite Rabs_left with (1 := Hx) in Hu. rewrite Rabs_left1 in Hu. now apply Ropp_le_cancel. apply Hxu1. apply HF. now apply Rlt_le. Qed.
imports: Coq(Reals) Raux Defs