proposition: Lemma pmin_le : forall (p:U) (n:nat), p - ([1/]1+n) <= pmin p n.
proof: Proof. unfold pmin; intros. apply Uminus_le_compat_right. induction n; simpl; intros; auto. apply Ole_trans with ([1/2] * ([1/]1+n)); auto. Qed.
imports: ALEA(Utheory)