proposition: Lemma graph_to_mat_inf: forall (g: @AdjMatGG size inf) u v, 0 <= u < v -> v < size -> ~ evalid g (u,v) -> Znth v (Znth u (graph_to_symm_mat g)) = inf.
proof: Proof. intros. unfold graph_to_symm_mat. rewrite <- elabel_Znth_graph_to_mat; try lia. rewrite eformat1. apply (MathAdjMatGraph.invalid_edge_weight); auto. simpl; lia. Qed.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.graph.MathUAdjMatGraph CertiGraph.graph.SpaceAdjMatGraph1 CertiGraph.lib.List_ext