proposition: Lemma Znth_nat_inc_list: forall {A: Type} {d: Inhabitant A} n (f: Z -> A) i, 0 <= i < Z.of_nat n -> Znth i (map f (nat_inc_list n)) = f i.
proof: Proof. intros. rewrite Znth_map. 2: rewrite Zlength_correct, nat_inc_list_length; auto. f_equal. induction n. - exfalso. simpl in H. intuition. - simpl. assert (0 <= i < Z.of_nat n \/ i = Z.of_nat n). { rewrite Nat2Z.inj_succ in H. destruct H. rewrite Z.lt_succ_r, Z.lt_eq_cases in H0. destruct H0; [left | right]; auto. } assert (Zlength (nat_inc_list n) = Z.of_nat n) by (rewrite Zlength_correct, nat_inc_list_length; auto). destruct H0. + rewrite app_Znth1. 2: rewrite H1; destruct H0; auto. apply IHn; auto. + rewrite app_Znth2. 2: rewrite H1; intuition. rewrite H0, H1. replace (Z.of_nat n - Z.of_nat n) with 0 by lia. rewrite Znth_0_cons. auto. 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