proposition: Lemma Rbar_lt_not_le (x y : Rbar) : Rbar_lt y x -> ~ Rbar_le x y.
proof: Proof. destruct x ; destruct y ; simpl ; intuition. apply (Rlt_irrefl r0). now apply Rlt_le_trans with (1 := H). Qed.
imports: Coq(Reals ssreflect) Rcomplements