proposition: Theorem fold_plus_permutation : forall (B : Type) (l1 l2 : list B) (c : nat) (f : B -> nat), Permutation l1 l2 -> fold_left (fun (a : nat) (b : B) => a + f b) l1 c = fold_left (fun (a : nat) (b : B) => a + f b) l2 c.
proof: Proof. intros B l1 l2 c f H; generalize c f; elim H; clear H l1 l2 c f; simpl in |- *; auto. intros a b L c f; repeat rewrite <- Nat.add_assoc; rewrite (Nat.add_comm (f a)); auto. intros L1 L2 L3 H H0 H1 H2 c f; apply trans_equal with (1 := H0 c f); auto. Qed.
imports: Coq(Sorting.Permutation)