proposition: Lemma sumList_filter : forall (A : Set)(ls : list A)(f : A -> Rat)(P : A -> bool) init, fold_left (fun r a => r + if (P a) then (f a) else 0) ls init == fold_left (fun r a => r + (f a)) (filter P ls) init.
proof: Proof. induction ls; simpl in *; intuition. destruct (P a); simpl. eapply IHls. rewrite fold_add_body_eq. eapply IHls. symmetry. eapply ratAdd_0_r. intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia