proposition: Lemma Rbar_finite_eq (x y : R) : Finite x = Finite y <-> x = y.
proof: Proof. split ; intros. apply Rle_antisym ; apply Rnot_lt_le ; intro. assert (Rbar_lt (Finite y) (Finite x)). simpl ; apply H0. rewrite H in H1 ; simpl in H1 ; by apply Rlt_irrefl in H1. assert (Rbar_lt (Finite x) (Finite y)). simpl ; apply H0. rewrite H in H1 ; simpl in H1 ; by apply Rlt_irrefl in H1. rewrite H ; reflexivity. Qed.
imports: Coq(Reals ssreflect) Rcomplements