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