proposition: Lemma nth_error_None_iff: forall {A} (l: list A) n, nth_error l n = None <-> n >= length l.
proof: Proof. intros. revert n; induction l; intros; destruct n; simpl. + split; [intros _; lia | auto]. + split; [intros _; lia | auto]. + split; [intros; inversion H | lia]. + rewrite IHl. 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