proposition: Lemma nat_inc_list_i: forall i n, 0 <= i < Z.of_nat n -> Znth i (nat_inc_list n) = i.
proof: Proof. intros. generalize dependent i. induction n. 1: intros; exfalso; destruct H; rewrite Nat2Z.inj_0 in H0; lia. intros. simpl. rewrite Nat2Z.inj_succ in H. destruct H. apply Zlt_succ_le in H0. apply Zle_lt_or_eq in H0. destruct H0. - rewrite app_Znth1. apply IHn. lia. now rewrite nat_inc_list_Zlength. - rewrite app_Znth2 by (rewrite nat_inc_list_Zlength; lia). rewrite H0. rewrite nat_inc_list_Zlength. simpl. replace (Z.of_nat n - Z.of_nat n) with 0 by lia. rewrite Znth_0_cons; trivial. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver