proposition: Lemma fold_add_nat_filter_partition : forall (A : Set)(P : A -> bool)(f : A -> nat)(ls : list A), fold_left (fun acc a => acc + (f a))%nat ls O = (plus (fold_left (fun acc a => acc + (f a))%nat (filter P ls) O) (fold_left (fun acc a => acc + (f a))%nat (filter (fun a => negb (P a)) ls) O) ).
proof: Proof. induction ls; intuition; simpl in *. destruct (P a); simpl; repeat rewrite (fold_add_init_nat _ _ (f a)). rewrite IHls. repeat rewrite Nat.add_assoc. trivial. rewrite IHls. repeat rewrite Nat.add_assoc. f_equal. rewrite Nat.add_comm. trivial. Qed.
imports: FCF.FCF Permutation