proposition: Theorem sumList_all : forall (A : Set)(ls : list A)(f : A -> Rat) c, (forall a, In a ls -> (f a) == c) -> sumList ls f == (length ls)/1 * c.
proof: Proof. induction ls; intuition. unfold sumList; simpl. symmetry. eapply ratMult_0_l. rewrite sumList_cons. simpl in *. rewrite H; intuition. rewrite IHls; intuition. rewrite ratMult_comm. rewrite ratMult_ratAdd_cd. simpl. eapply ratMult_comm. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation