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