proposition: Lemma fold_left_sum_acc : forall {A B} seq m n (f: A -> list B), m + fold_left (fun (count : nat) (x : A) => count + length (f x)) seq n = fold_left (fun (count : nat) (x : A) => count + length (f x)) seq (n + m).
proof: Proof. induction seq; simpl; intros; eauto with arith. rewrite IHseq; f_equal; eauto with arith. repeat rewrite <- Nat.add_assoc; f_equal; auto with arith. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts