proposition: Lemma sigma_fin_plus : forall (f g: A -> U) (P:A->Prop)(FP:finite P), sigma_fin (fun k => f k + g k) FP == sigma_fin f FP + sigma_fin g FP.
proof: Proof. induction FP; simpl; intros. repeat Usimpl; auto. rewrite IHFP. repeat norm_assoc_left; repeat Usimpl. repeat norm_assoc_right; repeat Usimpl; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)