proposition: Lemma sumList_app : forall (A : Set)(ls1 ls2 : list A)(f : A -> Rat), sumList (ls1 ++ ls2) f == (sumList ls1 f) + (sumList ls2 f).
proof: Proof. induction ls1; intuition; simpl in *. unfold sumList; simpl in *. rewrite <- ratAdd_0_l. intuition. repeat rewrite sumList_cons. rewrite IHls1. rewrite ratAdd_assoc. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation