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