proposition: Lemma Rbar_mult_pos_le (x y : Rbar) (z : posreal) : Rbar_le x y <-> Rbar_le (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 Rmult_le_compat_r with (2 := H). now apply Rlt_le. now apply Rmult_le_reg_r with (2 := H). Qed.
imports: Coq(Reals ssreflect) Rcomplements