proposition: Lemma sigma_plus_lift : forall (f :nat -> U) (n m:nat), sigma f (n+m)%nat == sigma f n + sigma (fun k => f (n+k)%nat) m.
proof: Proof. intros f n m; generalize f; clear f; induction n; intros. simpl plus. rewrite sigma_0. rewrite Uplus_zero_left. apply sigma_eq_compat; auto. rewrite sigma_S_lift. simpl plus. rewrite sigma_S_lift. rewrite IHn; auto. Qed.
imports: ALEA(Utheory)