proposition: Lemma Ule_nth_lim : forall x y, (forall p, x <= y + [1/]1+p) -> x <= y.
proof: Proof. intros; apply Ule_lt_lim; intros. apply (Ult_le_nth_minus H0); auto; intros n H1. apply Ole_trans with (x - [1/]1+n); auto. apply Ole_trans with (y + [1/]1+n - [1/]1+n); auto. Qed.
imports: ALEA(Utheory)