proposition: Lemma combine_nth_lt {A B}: forall (l1: list A) (l2: list B) n x y, n < length l1 -> n < length l2 -> nth n (combine l1 l2) (x, y) = (nth n l1 x, nth n l2 y).
proof: Proof. induction l1; intros. - simpl in *. exfalso. lia. - destruct l2. + simpl in H0. exfalso. lia. + simpl. destruct n; [|simpl in *; rewrite IHl1 by lia]; reflexivity. 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