proposition: Lemma sumList_iter_le : forall (A : Set)(ls : list A) f r a, sumList ls f <= r -> In a ls -> f a <= r.
proof: Proof. intuition. eapply fold_add_iter_le; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool