proposition: Lemma Rbar_mult_correct' (x y z : Rbar) : is_Rbar_mult x y z -> ex_Rbar_mult x y.
proof: Proof. unfold is_Rbar_mult ; case: x => [x | | ] ; case: y => [y | | ] //= ; case: Rle_dec => //= H ; try (case: Rle_lt_or_eq_dec => //=) ; intros. by apply Rgt_not_eq. by apply Rlt_not_eq, Rnot_le_lt. by apply Rgt_not_eq. by apply Rlt_not_eq, Rnot_le_lt. by apply Rgt_not_eq. by apply Rlt_not_eq, Rnot_le_lt. by apply Rgt_not_eq. by apply Rlt_not_eq, Rnot_le_lt. Qed.
imports: Coq(Reals ssreflect) Rcomplements