proposition: Lemma fold_add_eq_init : forall (A : Set)(ls : list A) init, fold_left (fun r a => r + 0) ls init == init.
proof: Proof. induction ls; intuition; simpl in *; intuition. eapply eqRat_trans. eapply fold_add_body_eq; intuition. rewrite <- ratAdd_0_r. apply eqRat_refl. apply eqRat_refl. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool