proposition: Theorem Rnd_N0_pt_unique : forall F : R -> Prop, F 0 -> forall x f1 f2 : R, Rnd_N0_pt F x f1 -> Rnd_N0_pt F x f2 -> f1 = f2.
proof: Proof. intros F HF x f1 f2 H1 H2. apply (Rnd_NG_pt_unique F _ (Rnd_N0_pt_unique_prop F HF) x). now apply -> Rnd_N0_NG_pt. now apply -> Rnd_N0_NG_pt. Qed.
imports: Coq(Reals) Raux Defs