proposition: Lemma sumList_filter_le : forall (A : Set)(ls : list A)(f : A -> Rat)(P : A -> bool), sumList (filter P ls) f <= sumList ls f.
proof: Proof. induction ls; intuition; unfold sumList in *; simpl in *. intuition. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. rewrite fold_add_body_eq. 2:{ eapply ratAdd_comm. } eapply fold_add_init. intuition. eapply eqRat_refl. } destruct (P a); simpl. rewrite fold_add_body_eq. 2:{ eapply ratAdd_comm. } 2:{ intuition. eapply eqRat_refl. } rewrite fold_add_init. eapply ratAdd_leRat_compat; intuition. rewrite ratAdd_0_l. eapply ratAdd_leRat_compat; intuition. eapply rat0_le_all. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation