proposition: Lemma Ult_le_nth_minus : forall x y, x < y -> exc (fun n => x <= y - [1/]1+n).
proof: Proof. intros; apply (archimedian (x:=(y - x))); intros; auto. apply exc_intro with x0. apply Uminus_le_perm; auto. apply Ole_trans with (y - x); auto. Qed.
imports: ALEA(Utheory)