proposition: Lemma sumList_rel_plus_inv : forall (A : Type)(ls : list A) r (rel1 rel2 rel : A -> Rat -> Prop), sumList_rel rel ls r -> (forall a r, In a ls -> rel a r -> forall r1 r2, rel1 a r1 -> rel2 a r2 -> r == r1 + r2) -> forall r1 r2, sumList_rel rel1 ls r1 -> sumList_rel rel2 ls r2 -> r == r1 + r2.
proof: Proof. induction ls; intuition; simpl in *. inversion H1; clear H1; subst. inversion H2; clear H2; subst. inversion H; clear H; subst. rewrite H3. rewrite H1. rewrite H2. rewrite <- ratAdd_0_l. intuition. inversion H1; clear H1; subst. inversion H2; clear H2; subst. inversion H; clear H; subst. assert (r7 == r3 + r5). eauto. assert (r6 == r0 + r4). eauto. rewrite H12. rewrite H8. rewrite H10. rewrite H. rewrite H1. repeat rewrite <- ratAdd_assoc. eapply ratAdd_eqRat_compat; intuition. rewrite ratAdd_assoc. rewrite (ratAdd_comm r5). rewrite <- ratAdd_assoc. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation