proposition: Theorem sumList_flatten : forall (A : Set)(ls : list (list A)) f, sumList (flatten ls) f == sumList ls (fun x => sumList x f).
proof: Proof. intuition idtac. apply fold_add_flatten. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation