proposition: Lemma is_Rbar_mult_m_infty_pos (x : Rbar) : Rbar_lt 0 x -> is_Rbar_mult m_infty x m_infty.
proof: Proof. case: x => [x | | ] // Hx. unfold is_Rbar_mult, Rbar_mult'. case: Rle_dec (Rlt_le _ _ Hx) => // Hx' _. now case: Rle_lt_or_eq_dec (Rlt_not_eq _ _ Hx). Qed.
imports: Coq(Reals ssreflect) Rcomplements