proposition: Lemma Rbar_mult'_opp_r (x y : Rbar) : Rbar_mult' x (Rbar_opp y) = match Rbar_mult' x y with Some z => Some (Rbar_opp z) | None => None end.
proof: Proof. case: x => [x | | ] ; case: y => [y | | ] //= ; (try case: Rle_dec => Hx //=) ; (try case: Rle_lt_or_eq_dec => //= Hx0). by rewrite Ropp_mult_distr_r_reverse. rewrite -Ropp_0 in Hx0. apply Ropp_lt_cancel in Hx0. case Rle_dec => Hy //=. now elim Rle_not_lt with (1 := Hy). case Rle_dec => Hy //=. case Rle_lt_or_eq_dec => Hy0 //=. elim Rlt_not_le with (1 := Hy0). apply Ropp_le_cancel. by rewrite Ropp_0. elim Hy. apply Ropp_le_cancel. rewrite -Hx0 Ropp_0. apply Rle_refl. case Rle_dec => Hy //=. case Rle_lt_or_eq_dec => Hy0 //=. elim Hx. rewrite -Hy0 Ropp_0. apply Rle_refl. elim Hx. rewrite -Ropp_0. apply Ropp_le_contravar. apply Rlt_le. now apply Rnot_le_lt. case Rle_dec => Hy //=. elim Rlt_not_le with (1 := Hx0). rewrite -Ropp_0. now apply Ropp_le_contravar. case Rle_dec => Hy //=. case Rle_lt_or_eq_dec => Hy0 //=. elim Rlt_not_le with (1 := Hy0). apply Ropp_le_cancel. rewrite -Hx0 Ropp_0. apply Rle_refl. elim Hy. apply Ropp_le_cancel. rewrite -Hx0 Ropp_0. apply Rle_refl. case Rle_dec => Hy //=. case Rle_lt_or_eq_dec => Hy0 //=. elim Hx. rewrite -Hy0 Ropp_0. apply Rle_refl. elim Hx. rewrite -Ropp_0. apply Ropp_le_contravar. apply Rlt_le. now apply Rnot_le_lt. Qed.
imports: Coq(Reals ssreflect) Rcomplements