proposition: Lemma sigma_plus : forall (f g : nat -> U) (n:nat), sigma (fun k => (f k) + (g k)) n == sigma f n + sigma g n.
proof: Proof. intros; induction n; simpl; auto. repeat rewrite sigma_S; setoid_rewrite IHn. repeat norm_assoc_right; apply Uplus_eq_compat_right. setoid_rewrite (Uplus_sym (g n) ((sigma f n) + (sigma g n))). repeat norm_assoc_right; apply Uplus_eq_compat_right; auto. Qed.
imports: ALEA(Utheory)