proposition: Lemma Rbar_le_lt_trans (x y z : Rbar) : Rbar_le x y -> Rbar_lt y z -> Rbar_lt x z.
proof: Proof. destruct x ; destruct y ; destruct z ; simpl ; intuition. now apply Rle_lt_trans with r0. Qed.
imports: Coq(Reals ssreflect) Rcomplements