proposition: Theorem Rnd_N_pt_idempotent : forall F : R -> Prop, forall x f : R, Rnd_N_pt F x f -> F x -> f = x.
proof: Proof. intros F x f (_,Hf) Hx. apply Rminus_diag_uniq. destruct (Req_dec (f - x) 0) as [H|H]. exact H. elim Rabs_no_R0 with (1 := H). apply Rle_antisym. replace 0 with (Rabs (x - x)). now apply Hf. unfold Rminus. rewrite Rplus_opp_r. apply Rabs_R0. apply Rabs_pos. Qed.
imports: Coq(Reals) Raux Defs