proposition: Lemma sumList_0 : forall (ls : list A) f, (sumList ls f == 0) <-> (forall a, In a ls -> (f a) == 0).
proof: Proof. induction ls; intuition; simpl in *. intuition. unfold sumList. simpl. eapply eqRat_refl. intuition; subst. unfold sumList in *; simpl in *. eapply eqRat_trans. eapply ratAdd_0. eapply eqRat_trans. eapply ratAdd_comm. eapply eqRat_trans. eapply eqRat_symm. eapply fold_add_init. eapply eqRat_trans. eapply fold_add_body_eq. eapply ratAdd_comm. intuition. eapply eqRat_refl. eapply H. eapply eqRat_refl. eapply IHls. unfold sumList in *; simpl in *. eapply ratAdd_0. eapply eqRat_trans. eapply eqRat_symm. eapply fold_add_init. eapply eqRat_trans. eapply fold_add_body_eq. eapply ratAdd_comm. intuition. eapply eqRat_refl. eapply H. trivial. unfold sumList. simpl. eapply eqRat_trans. eapply fold_add_body_eq. eapply ratAdd_comm. intuition. eapply eqRat_refl. eapply eqRat_trans. eapply fold_add_init. eapply ratAdd_0. intuition. unfold sumList in *. eapply IHls. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool