proposition: Lemma Rbar_mult_correct (x y : Rbar) : ex_Rbar_mult x y -> is_Rbar_mult x y (Rbar_mult x y).
proof: Proof. case: x => [x | | ] ; case: y => [y | | ] //= H ; apply sym_not_eq in H ; unfold is_Rbar_mult ; simpl ; case: Rle_dec => // H0 ; case: Rle_lt_or_eq_dec => //. Qed.
imports: Coq(Reals ssreflect) Rcomplements