proposition: Lemma sumList_filter_prod_eq_r : forall (eqd : eq_dec bool)(A : Set)(ls : list A)(p : A -> bool) f, sumList (filter p ls) f == sumList ls (fun a => (f a) * (if (eqd (p a) true) then 1 else 0)).
proof: Proof. intuition. symmetry. rewrite (sumList_filter_partition p0). eapply eqRat_trans. eapply ratAdd_eqRat_compat. eapply sumList_body_eq; intuition. apply filter_In in H. intuition. rewrite H1. destruct (eqd true true); try congruence. eapply ratMult_1_r. eapply sumList_0; intuition. apply filter_In in H. intuition. destruct (p0 a); simpl in *; try congruence. destruct (eqd false true); try congruence. eapply ratMult_0_r. symmetry. eapply ratAdd_0_r. Qed.
imports: Crypto FCF RndNat Asymptotic