proposition: Lemma graph_to_mat_Zlength: forall g (f : E -> E), 0 <= size -> Zlength (graph_to_mat g f) = size.
proof: Proof. intros. unfold graph_to_mat. rewrite Zlength_map, nat_inc_list_Zlength, Z2Nat.id; 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.mpred 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.MathEdgeLabelGraph