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