proposition: Lemma Rbar_mult_0_l (x : Rbar) : Rbar_mult 0 x = 0.
proof: Proof. case: x => [x | | ] //=. by rewrite Rmult_0_l. case: Rle_dec (Rle_refl 0) => // H _. case: Rle_lt_or_eq_dec (Rlt_irrefl 0) => // _ _. case: Rle_dec (Rle_refl 0) => // H _. case: Rle_lt_or_eq_dec (Rlt_irrefl 0) => // _ _. Qed.
imports: Coq(Reals ssreflect) Rcomplements