proposition: Lemma is_Rbar_mult_opp_l (x y z : Rbar) : is_Rbar_mult x y z -> is_Rbar_mult (Rbar_opp x) y (Rbar_opp z).
proof: Proof. case: x => [x | | ] ; case: y => [y | | ] ; case: z => [z | | ] //= ; unfold is_Rbar_mult, Rbar_mult' ; try (case: Rle_dec => // H) ; try (case: Rle_lt_or_eq_dec => // H0) ; try (case => <-) ; try (move => _). apply (f_equal (@Some _)), f_equal ; ring. apply Ropp_lt_contravar in H0 ; rewrite Ropp_0 in H0 ; now move/Rlt_not_le: H0 ; case: Rle_dec. apply Rnot_le_lt, Ropp_lt_contravar in H ; rewrite Ropp_0 in H ; move/Rlt_le: (H) ; case: Rle_dec => // H0 _ ; now move/Rlt_not_eq: H ; case: Rle_lt_or_eq_dec. apply Rnot_le_lt, Ropp_lt_contravar in H ; rewrite Ropp_0 in H ; move/Rlt_le: (H) ; case: Rle_dec => // H0 _ ; now move/Rlt_not_eq: H ; case: Rle_lt_or_eq_dec. apply Ropp_lt_contravar in H0 ; rewrite Ropp_0 in H0 ; now move/Rlt_not_le: H0 ; case: Rle_dec. Qed.
imports: Coq(Reals ssreflect) Rcomplements