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