proposition: Lemma Rbar_mult_pos_eq (x y : Rbar) (z : posreal) : x = y <-> (Rbar_mult_pos x z) = (Rbar_mult_pos y z).
proof: Proof. case: z => z Hz ; case: x => [x | | ] ; case: y => [y | | ] ; split => //= H ; apply Rbar_finite_eq in H. by rewrite H. apply Rbar_finite_eq, (Rmult_eq_reg_r (z)) => // ; by apply Rgt_not_eq. Qed.
imports: Coq(Reals ssreflect) Rcomplements