proposition: Lemma graph_to_list_Zlength: forall g (f : E -> E) n, 0 <= size -> 0 <= n -> Forall (fun list => Zlength list = n) (graph_to_mat g f) -> Zlength (graph_to_list g f) = size * n.
proof: Proof. intros. rewrite <- (Z2Nat.id size); trivial. unfold graph_to_list, graph_to_mat in *. apply Zlength_concat; trivial. 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