proposition: Lemma graph_to_mat_eq: forall (g: AdjMatLG) i j, 0 <= i < size -> 0 <= j < size -> (Znth i (Znth j (graph_to_symm_mat g))) = elabel g (eformat (i,j)).
proof: Proof. intros. symmetry. rewrite eformat_symm. apply elabel_Znth_graph_to_mat; lia. Qed.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.graph.MathUAdjMatGraph CertiGraph.graph.SpaceAdjMatGraph1 CertiGraph.lib.List_ext