proposition: Lemma le_p_lim_pmin : forall p, p <= lub (Pmin p).
proof: Proof. intro; apply Ule_lt_lim; intros. assert (exc (fun n : nat => t <= p - [1/]1+n)). apply Ult_le_nth_minus; trivial. apply H0; auto; intros n H1. apply Ole_trans with (p - [1/]1+n); auto. apply Ole_trans with (pmin p n); auto. apply le_lub with (f:=Pmin p) (n:=n). Qed.
imports: ALEA(Utheory)