proposition: Lemma sumList_filter_partition : forall (A : Set)(P : A -> bool)(ls : list A)(f : A -> Rat), sumList ls f == (sumList (filter P ls) f + (sumList (filter (fun a => negb (P a)) ls) f)).
proof: Proof. induction ls; intuition; simpl in *. unfold sumList. simpl. eapply ratAdd_0_l. unfold sumList in *. simpl in *. erewrite fold_add_body_eq. 2:{ eapply ratAdd_comm. } 2:{ intuition. eapply eqRat_refl. } rewrite fold_add_init. destruct (P a); simpl. erewrite (fold_add_body_eq (filter P ls)). 2:{ eapply ratAdd_comm. } 2:{ intuition. eapply eqRat_refl. } rewrite fold_add_init. rewrite ratAdd_assoc. eapply ratAdd_eqRat_compat; intuition. erewrite (fold_add_body_eq (filter (fun a => negb (P a)) ls)). 2:{ eapply ratAdd_comm. } 2:{ intuition. eapply eqRat_refl. } rewrite fold_add_init. rewrite <- ratAdd_assoc. rewrite (ratAdd_comm (fold_left (fun (a0 : Rat) (b : A) => a0 + f b) (filter P ls) 0 )). rewrite ratAdd_assoc. eapply ratAdd_eqRat_compat; intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation