proposition: Lemma Rbar_plus_opp (x y : Rbar) : Rbar_plus (Rbar_opp x) (Rbar_opp y) = Rbar_opp (Rbar_plus x y).
proof: Proof. case: x => [x | | ] ; case: y => [y | | ] //= ; apply f_equal ; ring. Qed.
imports: Coq(Reals ssreflect) Rcomplements