proposition: Lemma sumList_rel_permutation : forall (A : Type)(rel : A -> Rat -> Prop)(ls1 ls2 : list A), Permutation ls1 ls2 -> forall r, sumList_rel rel ls1 r -> sumList_rel rel ls2 r.
proof: Proof. induction 1; intuition; simpl in *. inversion H0; clear H0; subst. econstructor; eauto. inversion H; clear H; subst. inversion H2; clear H2; subst. econstructor; eauto. econstructor; eauto. eapply eqRat_refl. rewrite H5. rewrite H7. repeat rewrite <- ratAdd_assoc. eapply ratAdd_eqRat_compat; intuition. eapply ratAdd_comm. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation