proposition: Lemma fold_add_permutation : forall (A : Set) ls1 ls2, Permutation ls1 ls2 -> forall (f : A -> Rat) init1 init2, init1 == init2 -> fold_left (fun r a => r + (f a)) ls1 init1 == fold_left (fun r a => r + (f a)) ls2 init2.
proof: Proof. induction 1; intuition; simpl in *. eapply IHPermutation. eapply ratAdd_eqRat_compat; intuition. rewrite fold_add_body_eq. eapply eqRat_refl. rewrite ratAdd_assoc. rewrite (ratAdd_comm (f y)). rewrite <- ratAdd_assoc. intuition. eapply ratAdd_eqRat_compat; intuition. eapply ratAdd_eqRat_compat; intuition. intuition. eapply eqRat_trans. eapply IHPermutation1. eapply H1. eapply IHPermutation2. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation