proposition: Lemma length_flatten_aux : forall {A} seq, forall n, n + List.length (flatten seq) = List.fold_right (compose plus (@List.length A)) n seq.
proof: Proof. induction seq; simpl; intros. - auto with arith. - unfold compose; rewrite app_length, <- IHseq. rewrite Nat.add_comm, <- Nat.add_assoc; auto with arith. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Fiat.Common Coq.Arith.Arith