proposition: Lemma sumList_rel_all_0 : forall (A : Type)(rel : A -> Rat -> Prop)(ls : list A), (forall a, In a ls -> rel a 0) -> sumList_rel rel ls 0.
proof: Proof. induction ls; intuition; simpl in *. econstructor. intuition. econstructor. eapply IHls. intuition. eauto. rewrite <- ratAdd_0_l. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation