proposition: Lemma sumList_rel_only_one_inv : forall (A : Set)(rel : A -> Rat -> Prop)(ls : list A)(a : A) r r', sumList_rel rel ls r' -> In a ls -> NoDup ls -> (forall a', In a' ls -> a <> a' -> forall v, rel a' v -> v == 0) -> (forall v, rel a v -> v == r) -> r' == r.
proof: Proof. induction ls; intuition; simpl in *. intuition. inversion H1; clear H1; subst. inversion H; clear H; subst. intuition; subst. rewrite H10. rewrite (H3 r2); eauto. rewrite (sumList_rel_all_0_inv H5). rewrite <- ratAdd_0_r. intuition. intuition. eapply H2. right. eauto. intuition; subst. eauto. trivial. eapply eqRat_trans. rewrite H10. eapply ratAdd_eqRat_compat. eapply H2. left. eauto. intuition; subst; intuition. trivial. eauto. rewrite <- ratAdd_0_l. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation