proposition: Lemma sumList_filter_twice : forall (A B : Set)(P : A -> bool)(ls : list A)(lsf : A -> list B)(f : A * B -> Rat), sumList (filter (fun p => P (fst p)) (flatten (map (fun a => map (fun b => (a, b)) (lsf a)) ls))) f == sumList (filter P ls) (fun a => sumList (lsf a) (fun b => f (a, b))).
proof: Proof. induction ls; intuition; simpl in *. unfold sumList. simpl. intuition. case_eq (P a); intuition. rewrite sumList_cons. rewrite filter_app. rewrite sumList_app. eapply ratAdd_eqRat_compat; intuition. rewrite filter_all_true. eapply sumList_map. intuition. apply in_map_iff in H0. destruct H0. intuition. subst. simpl. trivial. rewrite filter_app. rewrite sumList_app. symmetry. rewrite ratAdd_0_l. symmetry. eapply ratAdd_eqRat_compat; intuition. eapply sumList_0; intuition. apply filter_In in H0. intuition. apply in_map_iff in H1. destruct H1. intuition. subst. simpl in *. congruence. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation