proposition: Lemma length_flat_map : forall {A B} seq (f: A -> list B), List.length (flat_map f seq) = fold_left (fun count (x : A) => count + List.length (f x)) seq 0.
proof: Proof. simpl; induction seq; simpl; intros; eauto. rewrite app_length, IHseq; clear. apply fold_left_sum_acc. 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