proposition: Lemma Unth_sigma_Sn : forall n : nat, 1 == sigma (fun k => [1/]1+n) (S n).
proof: Proof. intros; rewrite sigma_S. apply Oeq_trans with ([1-] (sigma (fun k => [1/]1+n) n) + (sigma (fun k => [1/]1+n) n));auto. Qed.
imports: ALEA(Utheory)