proposition: Lemma Rbar_mult_opp_r (x y : Rbar) : Rbar_mult x (Rbar_opp y) = (Rbar_opp (Rbar_mult x y)).
proof: Proof. unfold Rbar_mult. rewrite Rbar_mult'_opp_r. case Rbar_mult' => //=. apply f_equal, eq_sym, Ropp_0. Qed.
imports: Coq(Reals ssreflect) Rcomplements