proposition: Lemma fold_add_eq : forall (A : Set)(ls : list A)(f1 f2 : A -> Rat) init1 init2, fold_left (fun r a => r + (f1 a)) ls init1 + fold_left (fun r a => r + (f2 a)) ls init2 == fold_left (fun r a => r + (f1 a + f2 a)) ls (init1 + init2).
proof: Proof. induction ls; intuition; simpl in *. eapply eqRat_refl. rewrite IHls. eapply fold_add_body_eq. repeat rewrite <- ratAdd_assoc. apply ratAdd_eqRat_compat; intuition. rewrite ratAdd_assoc. rewrite ratAdd_assoc. apply ratAdd_eqRat_compat; intuition. eapply ratAdd_comm. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool