proposition: Theorem Rnd_UP_pt_idempotent : forall F : R -> Prop, forall x f : R, Rnd_UP_pt F x f -> F x -> f = x.
proof: Proof. intros F x f (_,(Hx1,Hx2)) Hx. apply Rle_antisym. apply Hx2. exact Hx. apply Rle_refl. exact Hx1. Qed.
imports: Coq(Reals) Raux Defs