proposition: Lemma is_Rbar_mult_opp_r (x y z : Rbar) : is_Rbar_mult x y z -> is_Rbar_mult x (Rbar_opp y) (Rbar_opp z).
proof: Proof. move/is_Rbar_mult_sym => H. now apply is_Rbar_mult_sym, is_Rbar_mult_opp_l. Qed.
imports: Coq(Reals ssreflect) Rcomplements