proposition: Lemma list_size_fold : forall (A : Set) (size : A -> nat) l n, fold_left (fun (size_acc : nat) (a : A) => size_acc + size a) l n = n + list_size size l.
proof: Proof. intros A size l; induction l; trivial. intro n; simpl; rewrite Nat.add_assoc; apply IHl. Qed.
imports: Coq(List Arith)