proposition: Lemma upd_Znth_repeat: forall {A} (i:Z) size (a b : A), (0 <= i < size)%Z -> upd_Znth i (repeat a (Z.to_nat i) ++ repeat b (Z.to_nat (size - i))) a = repeat a (Z.to_nat (i + 1)) ++ repeat b (Z.to_nat (size - (i + 1))).
proof: Proof. intros. rewrite upd_Znth_app2. 2: repeat rewrite Zlength_repeat; lia. rewrite Zlength_repeat by lia. replace (i-i)%Z with 0%Z by lia. rewrite <- repeat_app' by lia. rewrite app_assoc_reverse; f_equal. rewrite upd_Znth0_old. 2: rewrite Zlength_repeat; lia. rewrite Zlength_repeat, sublist_repeat by lia. rewrite repeat1, Z.sub_add_distr. easy. 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