proposition: Lemma Rbar_plus_correct (x y : Rbar) : ex_Rbar_plus x y -> is_Rbar_plus x y (Rbar_plus x y).
proof: Proof. unfold is_Rbar_plus, ex_Rbar_plus, Rbar_plus. by case: Rbar_plus'. Qed.
imports: Coq(Reals ssreflect) Rcomplements