proposition: Lemma sublist_overshoot: forall {A:Type} (l: list A) lo hi, Zlength l <= lo -> sublist lo hi l = nil.
proof: Proof. intros. unfold sublist. rewrite skipn_short; auto. rewrite <- ZtoNat_Zlength. rewrite Zlength_firstn. destruct (Z.lt_trichotomy 0 hi). rewrite Z.max_r by lia. destruct (Z.lt_trichotomy hi (Zlength l)). rewrite Z.min_l. lia. lia. destruct H1. subst hi. rewrite Z.min_id. lia. rewrite Z.min_r by lia. lia. destruct H0. subst hi. rewrite Z.max_id. rewrite Z.min_l. lia. pose proof (Zlength_nonneg l); lia. rewrite Z.max_l by lia. rewrite Z.min_l. lia. pose proof (Zlength_nonneg l); 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