proposition: Lemma sumList_comm : forall (A B : Set)(lsa : list A)(lsb : list B) f, sumList lsa (fun a => sumList lsb (fun b => (f a b))) == sumList lsb (fun b => sumList lsa (fun a => (f a b))).
proof: Proof. intuition. eapply fold_add_comm; intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool