proposition: Lemma ex_Rbar_mult_opp_r (x y : Rbar) : ex_Rbar_mult x y -> ex_Rbar_mult x (Rbar_opp y).
proof: Proof. case: x => [x | | ] ; case: y => [y | | ] //= Hx ; by apply Ropp_neq_0_compat. Qed.
imports: Coq(Reals ssreflect) Rcomplements