proposition: Lemma nth_error_Some_In_combineP {X: Type} {i} {x: X} {L: list X} : nth_error L i = Some x <-> In (i, x) (combine (seq 0 (length L)) L).
proof: Proof. rewrite nth_error_combine_SomeP. split; first by apply: nth_error_In. move=> /(@In_nth_error (nat * X)) [j Hj]. suff: j = i. { move=> ?. by subst j. } suff: forall k, nth_error (combine (seq k (length L)) L) j = Some (i, x) -> k + j = i. { move=> /(_ 0). by apply. } clear Hj. elim: L j i; first by case. move=> y L IH [|j] i /= ? => [[]|/IH]; lia. Qed.
imports: PeanoNat List Lia Undecidability.StackMachines.Util.Nat_facts ssreflect ssrbool ssrfun