proposition: Lemma combine_Znth: forall {A B : Type} {I: Inhabitant A} {I: Inhabitant B} (l : list A) (l' : list B) (n : Z), length l = length l' -> 0 <= n < Zlength l -> Znth n (combine l l') = (Znth n l, Znth n l').
proof: Proof. intros. repeat rewrite <- nth_Znth. all: rewrite Zlength_correct in *; try rewrite combine_length; try rewrite <- H; try rewrite Nat.min_id; trivial. apply combine_nth; trivial. Qed.
imports: Coq.ZArith.BinInt Coq.ZArith.Zcomplements Coq.micromega.Lia Coq.ZArith.Znat compcert.lib.Integers compcert.common.Values compcert.export.Clightdefs VST.veric.mpred VST.zlist.sublist VST.floyd.field_at VST.floyd.coqlib3 VST.msl.iter_sepcon VST.msl.seplog CertiGraph.graph.graph_model CertiGraph.lib.List_ext CertiGraph.graph.MathEdgeLabelGraph