proposition: Lemma fold_add_factor_constant_r : forall (A : Set)(ls : list A)(f : A -> Rat) init c, fold_left (fun r a => r + (f a) * c) ls (init * c) == (fold_left (fun r a => r + (f a)) ls init) * c.
proof: Proof. induction ls; intuition; simpl in *. intuition. eapply eqRat_trans. eapply fold_add_body_eq. eapply eqRat_symm. eapply ratMult_distrib_r. intuition. eapply eqRat_refl. eapply IHls. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool