proposition: Lemma sumList_nz : forall (ls : list A) f, (~sumList ls f == 0) <-> exists a : _, In a ls /\ (~f a == 0).
proof: Proof. induction ls; intuition; unfold sumList in *; simpl in *. exfalso. apply H. eapply eqRat_refl. destruct H. intuition. assert (f a + fold_left (fun r a => r + f a) ls 0 == 0 -> False). intuition. eapply H. eapply eqRat_trans. eapply fold_add_body_eq. eapply ratAdd_comm. intuition. eapply eqRat_refl. eapply eqRat_trans. eapply fold_add_init. trivial. eapply ratAdd_nz in H0. destruct H0. econstructor; intuition. apply IHls in H0. destruct H0; intuition. exists x. intuition. assert (f a + fold_left (fun r a => r + f a) ls 0 == 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. trivial. apply ratAdd_0 in H1. intuition. destruct H. intuition. subst. intuition. apply IHls in H3; intuition. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool