proposition: Lemma elabel_Znth_graph_to_mat: forall (g: AdjMatLG) (f: E -> E) src dst, 0 <= size -> 0 <= src < size -> 0 <= dst < size -> elabel g (f (src, dst)) = Znth dst (Znth src (graph_to_mat g f)).
proof: Proof. intros. unfold graph_to_mat. rewrite Znth_map, nat_inc_list_i. unfold vert_to_list. rewrite Znth_map. rewrite Znth_map. rewrite nat_inc_list_i. reflexivity. 3: rewrite Zlength_map. 2, 3, 5: rewrite nat_inc_list_Zlength. all: rewrite Z2Nat.id; trivial. Qed.
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