proposition: Lemma Rnd_N0_pt_unique_prop : forall F : R -> Prop, F 0 -> Rnd_NG_pt_unique_prop F (fun x f => Rabs f <= Rabs x).
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 Hxd1. apply Hxu1. rewrite Rabs_pos_eq with (1 := Hx) in Hu. rewrite Rabs_pos_eq in Hu. exact Hu. apply Rle_trans with (1:=Hx). apply Hxu1. apply Hxu1. apply Hxd1. rewrite Rabs_left with (1 := Hx) in Hd. rewrite Rabs_left1 in Hd. now apply Ropp_le_cancel. apply Rlt_le, Rle_lt_trans with (2:=Hx). apply Hxd1. Qed.
imports: Coq(Reals) Raux Defs