proposition: Lemma sumList_subset : forall (A : Set)(eqd : eq_dec A)(ls1 ls2 : list A)(f : A -> Rat), NoDup ls1 -> NoDup ls2 -> (forall a, In a ls1 -> In a ls2) -> (forall a, (~In a ls1) -> (f a) == 0) -> sumList ls1 f == sumList ls2 f.
proof: Proof. intuition. eapply fold_add_subset; intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation