proposition: Lemma sigma_S_lift : forall (f :nat -> U) (n:nat), sigma f (S n) == (f O) + (sigma (fun k => f (S k)) n).
proof: Proof. intros f n; generalize f; induction n; intros; auto. rewrite sigma_S. rewrite IHn. rewrite sigma_S. rewrite Uplus_assoc. rewrite (Uplus_sym (f0 (S n)) (f0 O)); auto. Qed.
imports: ALEA(Utheory)