proposition: Lemma Rbar_eq_dec (x y : Rbar) : {x = y} + {x <> y}.
proof: Proof. intros ; destruct (Rbar_total_order x y) as [[H|H]|H]. right ; revert H ; destruct x as [x| |] ; destruct y as [y| |] ; simpl ; intros H ; try easy. contradict H. apply Rbar_finite_eq in H ; try apply Rle_not_lt, Req_le ; auto. left ; apply H. right ; revert H ; destruct x as [x| |] ; destruct y as [y| |] ; simpl ; intros H ; try easy. contradict H. apply Rbar_finite_eq in H ; apply Rle_not_lt, Req_le ; auto. Qed.
imports: Coq(Reals ssreflect) Rcomplements