proposition: Lemma sumList_factor_constant_r : forall (A : Set)(ls : list A)(f : A -> Rat) c, sumList ls (fun a => (f a) * c) == (sumList ls f) * c.
proof: Proof. intuition. unfold sumList. rewrite <- fold_add_factor_constant_r. eapply fold_add_body_eq. eapply eqRat_symm. eapply ratMult_0_l. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool