proposition: Lemma is_Rbar_mult_sym (x y z : Rbar) : is_Rbar_mult x y z -> is_Rbar_mult y x 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 => _). by rewrite Rmult_comm. Qed.
imports: Coq(Reals ssreflect) Rcomplements