fact: Definition graph_to_list (g: AdjMatLG) (f : E -> E) : list Z := (concat (graph_to_mat g f)).
imports: Coq.ZArith.BinInt Coq.ZArith.Zcomplements Coq.micromega.Lia Coq.ZArith.Znat VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.lib.List_ext CertiGraph.graph.MathAdjMatGraph