proposition: Lemma Rbar_opp_eq (x y : Rbar) : (Rbar_opp x) = (Rbar_opp y) <-> x = y.
proof: Proof. split ; intros H. rewrite <- (Rbar_opp_involutive x), H, Rbar_opp_involutive ; reflexivity. rewrite H ; reflexivity. Qed.
imports: Coq(Reals ssreflect) Rcomplements