proposition: Lemma fold_add_rat_perm : forall (ls1 ls2 : list A)(f1 f2 : A -> Rat), Permutation ls1 ls2 -> forall init1 init2, init1 == init2 -> (forall (a : A), In a ls1 -> (f1 a) == (f2 a)) -> fold_left (fun r a => r + (f1 a)) ls1 init1 == fold_left (fun r a => r + (f2 a)) ls2 init2.
proof: Proof. induction 1; intuition; simpl in *. eapply IHPermutation; eauto. eapply ratAdd_eqRat_compat; eauto. eapply fold_add_body_eq. eapply eqRat_trans. eapply ratAdd_assoc. eapply eqRat_trans. 2:{ eapply eqRat_symm. eapply ratAdd_assoc. } eapply ratAdd_eqRat_compat; eauto. eapply eqRat_trans. eapply ratAdd_comm. eapply ratAdd_eqRat_compat; eauto. intuition. eapply eqRat_trans; eauto. eapply eqRat_trans. eapply fold_add_body_eq. eapply eqRat_symm; eauto. intuition. eapply eqRat_symm. eapply H2. eapply Permutation_in. eapply Permutation_sym. eauto. eauto. simpl. eapply IHPermutation2. trivial. intuition. eapply H2. eapply Permutation_in. eapply Permutation_sym. eauto. eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool