proposition: Lemma nat_inc_list_sublist: forall n m, 0 <= n -> n <= m -> sublist 0 n (nat_inc_list (Z.to_nat m)) = nat_inc_list (Z.to_nat n).
proof: Proof. intros. apply Zle_lt_or_eq in H0. destruct H0. 2: { subst. rewrite sublist_same; trivial. rewrite nat_inc_list_Zlength; lia. } apply Znth_eq_ext. 1: { rewrite Zlength_sublist; try rewrite nat_inc_list_Zlength; lia. } intros. rewrite nat_inc_list_i. 2: { rewrite Zlength_sublist in H1; try rewrite nat_inc_list_Zlength; lia. } rewrite <- Z.sub_0_r at 1. replace n with (0 + n) by lia. rewrite Zlength_sublist in H1. rewrite <- nat_inc_list_app. rewrite nat_inc_list_i. all: try rewrite nat_inc_list_Zlength; lia. 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