proposition: Lemma Ult_le_nth_plus : forall x y, x < y -> exc (fun n : nat => x + [1/]1+n <= y).
proof: Proof. intros. assert (not (0==y-x)); auto. assert (H1:exc (fun n => [1/]1+n <= y - x)). apply archimedian; auto. apply H1;auto; intros n H2. apply exc_intro with n. apply Ole_trans with (x + (y - x)); auto. Qed.
imports: ALEA(Utheory)