proposition: Lemma Nth_split : forall n l x y r s, Nth n l (x,y) -> (r,s) = split l -> Nth n r x /\ Nth n s y.
proof: Proof. Proof using. Hint Constructors Nth. introv N E. gen_eq p: (x,y). gen r s x y. induction N as [l' [x' y']|[x' y'] n' l' [x'' y'']]; intros. { inverts EQp. rewrite split_cons_let in E. destruct (split l') as [r' s']. inverts* E. } { inverts EQp. rewrite split_cons_let in E. destruct (split l') as [r' s']. forwards*: IHN. inverts* E. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)