proposition: Lemma sumList_partition : forall (A : Set)(P : A -> bool)(ls : list A)(f : A -> Rat), sumList ls f == sumList ls (fun a => (f a) * (if (P a) then 1 else 0)) + sumList ls (fun a => (f a) * (if (P a) then 0 else 1)).
proof: Proof. induction ls; intuition. unfold sumList; simpl in *. eapply ratAdd_0_l. repeat rewrite sumList_cons. destruct (P a); rewrite ratMult_0_r; rewrite <- ratAdd_0_l; rewrite ratMult_1_r; rewrite IHls. rewrite ratAdd_assoc. intuition. rewrite (ratAdd_comm (sumList ls (fun a0 : A => f a0 * (if P a0 then 1 else 0)))). rewrite <- ratAdd_assoc. rewrite <- ratAdd_comm. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation