proposition: Lemma sumList_exactly_one : forall (A : Set) a (ls : list A) f, NoDup ls -> In a ls -> (forall b, In b ls -> a <> b -> f b == 0) -> sumList ls f == f a.
proof: Proof. induction ls; intuition. inversion H0. simpl in *. inversion H; clear H; subst. intuition; subst. assert (sumList ls f == 0). eapply sumList_0. intuition. eapply H1. intuition. intuition; subst; intuition. unfold sumList in *; simpl. rewrite fold_add_body_eq. 2:{ eapply ratAdd_comm. } rewrite fold_add_init. rewrite H. rewrite <- ratAdd_0_r. intuition. intuition. assert (sumList ls f == f a). eapply IHls; intuition. unfold sumList in *. simpl. rewrite fold_add_body_eq. 2:{ eapply ratAdd_comm. } rewrite fold_add_init. rewrite H0. rewrite H1. rewrite <- ratAdd_0_l. intuition. intuition. intuition; subst; intuition. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation