proposition: Lemma Rbar_lt_not_eq (x y : Rbar) : Rbar_lt x y -> x<>y.
proof: Proof. destruct x ; destruct y ; simpl ; try easy. intros H H0. apply Rbar_finite_eq in H0 ; revert H0 ; apply Rlt_not_eq, H. Qed.
imports: Coq(Reals ssreflect) Rcomplements