proposition: Lemma sumList_rel_all_0_inv : forall (A : Set)(ls : list A)(r : Rat)(rel : A -> Rat -> Prop), sumList_rel rel ls r -> (forall a' v, In a' ls -> rel a' v -> v == 0) -> r == 0.
proof: Proof. induction ls; intuition; simpl in *. inversion H. intuition. inversion H; clear H; subst. rewrite H6. rewrite (H0 a r2); eauto. rewrite <- ratAdd_0_l. eapply IHls; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation