proposition: Theorem Rnd_NG_pt_unique : forall (F : R -> Prop) (P : R -> R -> Prop), Rnd_NG_pt_unique_prop F P -> forall x f1 f2 : R, Rnd_NG_pt F P x f1 -> Rnd_NG_pt F P x f2 -> f1 = f2.
proof: Proof. intros F P HP x f1 f2 (H1a,H1b) (H2a,H2b). destruct H1b as [H1b|H1b]. destruct H2b as [H2b|H2b]. destruct (Rnd_N_pt_DN_or_UP _ _ _ H1a) as [H1c|H1c] ; destruct (Rnd_N_pt_DN_or_UP _ _ _ H2a) as [H2c|H2c]. eapply Rnd_DN_pt_unique ; eassumption. now apply (HP x f1 f2). apply sym_eq. now apply (HP x f2 f1 H2c H2a H1c H1a). eapply Rnd_UP_pt_unique ; eassumption. now apply H2b. apply sym_eq. now apply H1b. Qed.
imports: Coq(Reals) Raux Defs