proposition: Lemma nth_split : forall `{IA:Inhab A} `{IB:Inhab B} n l (r:list A) (s:list B), (r,s) = split l -> n < length l -> nth n l = (nth n r, nth n s).
proof: Proof. Proof using. introv E N. applys nth_of_Nth. lets ([x y]&M): Nth_inbound_inv N. forwards (F1&F2): Nth_split M E. rewrite (nth_of_Nth F1). rewrite~ (nth_of_Nth F2). Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)