proposition: Lemma Rbar_opp_minus (x y : Rbar) : Rbar_opp (Rbar_minus x y) = Rbar_minus y x.
proof: Proof. case: x => [x | | ] ; case: y => [y | | ] //=. by rewrite Ropp_minus_distr'. by rewrite Ropp_0. by rewrite Ropp_0. Qed.
imports: Coq(Reals ssreflect) Rcomplements