proposition: Lemma half_Unth: forall n, ([1/2])*([1/]1+n) <= [1/]1+(S n).
proof: Proof. intros; apply half_le; auto. rewrite (Unth_prop_sigma n). apply Ole_trans with ([1-] (sigma (fun _ : nat => [1/]1+(S n)) n)). apply Uinv_le_compat. apply sigma_le_compat; auto. apply Ole_trans with ([1-] (sigma (fun _ : nat => [1/]1+(S n)) (S n)) + [1/]1+(S n)); auto. Qed.
imports: ALEA(Utheory)