proposition: Lemma Ule_lt_lim : forall x y, (forall t, t < x -> t <= y) -> x <= y.
proof: Proof. intros; apply Ule_class; red; intros. pose (z:= mean y x). assert (y < z); unfold z; auto. apply H1; apply H; unfold z; auto. Qed.
imports: ALEA(Utheory)