proposition: Lemma Unth_decr : forall n, [1/]1+(S n) < [1/]1+n.
proof: Proof. repeat red; intros. apply (Unth_sigma_n (S n)). apply Ole_antisym; auto. apply Ole_trans with (sigma (fun _ : nat => [1/]1+n) (S n)); auto. Qed.
imports: ALEA(Utheory)