proposition: Theorem fold_plus_split : forall (B : Type) (l : list B) (c : nat) (f : B -> nat), c + fold_left (fun (a : nat) (b : B) => a + f b) l 0 = fold_left (fun (a : nat) (b : B) => a + f b) l c.
proof: Proof. intros B l; elim l; simpl in |- *; auto. intros a l0 H c f. rewrite <- (H (f a)). rewrite <- (H (c + f a)). rewrite Nat.add_assoc; auto. Qed.
imports: Coq(Sorting.Permutation)