proposition: Lemma is_Rbar_plus_unique (x y z : Rbar) : is_Rbar_plus x y z -> Rbar_plus x y = z.
proof: Proof. unfold is_Rbar_plus, ex_Rbar_plus, Rbar_plus. case: Rbar_plus' => // a Ha. by inversion Ha. Qed.
imports: Coq(Reals ssreflect) Rcomplements