proposition: Lemma Zlength_concat: forall size n f, 0 <= n -> Forall (fun list : list Z => Zlength list = n) (map f (nat_inc_list size)) -> Zlength (concat (map f (nat_inc_list size))) = Z.of_nat size * n.
proof: Proof. intros. clear H. induction size0. 1: simpl; apply Zlength_nil. rewrite Nat2Z.inj_succ, Z.mul_succ_l. simpl. rewrite map_app, concat_app, Zlength_app. simpl. rewrite app_nil_r. f_equal. - apply IHsize0. rewrite Forall_forall in H0 |- *. intros. apply H0. simpl. rewrite map_app. apply in_or_app; left; trivial. - rewrite Forall_forall in H0. apply H0. apply in_map. rewrite nat_inc_list_in_iff. lia. Qed.
imports: Coq.ZArith.BinInt Coq.ZArith.Zcomplements Coq.micromega.Lia Coq.ZArith.Znat compcert.lib.Integers compcert.common.Values compcert.export.Clightdefs VST.veric.expr VST.veric.mpred VST.floyd.forward VST.zlist.sublist VST.floyd.field_at VST.floyd.coqlib3 VST.msl.iter_sepcon VST.msl.seplog CertiGraph.graph.graph_model CertiGraph.lib.List_ext CertiGraph.graph.MathAdjMatGraph