proposition: Theorem sumList_prod : forall (A B : Set)(lsa : list A)(lsb : list B)(fa : A -> Rat)(fb : B -> Rat), (sumList lsa fa) * (sumList lsb fb) == (sumList lsa (fun a => (fa a) * sumList lsb fb)).
proof: Proof. intuition idtac. eapply fold_add_prod. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation