proposition: Lemma bounded_vertex: forall v n, 0 <= v < n -> n <= Int.max_signed / 8 -> Int.min_signed <= v <= Int.max_signed.
proof: Proof. intros. destruct H. split. - apply Z.le_trans with 0; auto. rewrite Z.lt_eq_cases. left. apply Int.min_signed_neg. - apply Z.le_trans with n. 1: rewrite Z.lt_eq_cases; left; auto. apply Z.le_trans with (Int.max_signed / 8); auto. rewrite Z.lt_eq_cases; left. apply Z_div_lt; intuition. Qed.
imports: CertiGraph.lib.List_ext CertiGraph.unionfind.env_unionfind_arr CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.graph.UnionFind CertiGraph.msl_application.ArrayGraph CertiGraph.floyd_ext.share CertiGraph.unionfind.spatial_array_graph Coq.Lists.List CertiGraph.unionfind.uf_arr_specs VST.floyd.library