proposition: Lemma uniqueness_dec P : (exists ! x : R, P x) -> {x : R | P x}.
proof: Proof. move => H. exists (Lub_Rbar P). case: H => x Hx. replace (real (Lub_Rbar P)) with (real (Finite x)). by apply Hx. apply f_equal, sym_eq, is_lub_Rbar_unique. split. move => y Hy. right ; by apply sym_eq, Hx. move => b Hb. by apply Hb, Hx. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov