proposition: Lemma fold_add_init_0 : forall (A : Set)(ls : list A) f init, fold_left (fun r a => r + (f a)) ls init == init + fold_left (fun r a => r + (f a)) ls 0.
proof: Proof. intuition. eapply eqRat_trans. eapply fold_add_body_eq; intuition. rewrite ratAdd_0_r. apply eqRat_refl. apply eqRat_refl. apply fold_add_init. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool