proposition: Lemma Rbar_mult_eq_0 (y x : Rbar) : Rbar_mult x y = 0 -> x = 0 \/ y = 0.
proof: Proof. case: x => [x | | ] //= ; case: y => [y | | ] //= ; (try case: Rle_dec => //= H) ; (try case: Rle_lt_or_eq_dec => //=) ; (try (left ; by apply f_equal)) ; (try (right ; by apply f_equal)). intros H. apply (f_equal real) in H. simpl in H. apply Rmult_integral in H ; case: H => ->. by left. by right. Qed.
imports: Coq(Reals ssreflect) Rcomplements