proposition: Lemma sumList_factor_constant_l: forall (A : Set) (ls : list A) (f : A -> Rat) (c : Rat), sumList ls (fun a : A => c * f a) == c * sumList ls f.
proof: Proof. intuition. eapply eqRat_trans. eapply sumList_body_eq; intuition. apply ratMult_comm. eapply eqRat_trans. eapply sumList_factor_constant_r. apply ratMult_comm. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool