proposition: Lemma nth_split_l : forall `{IA:Inhab A} `{IB:Inhab B} n l (r:list A) (s:list B), (r,s) = split l -> n < length l -> nth n r = fst (nth n l).
proof: Proof. Proof using. introv E N. rewrites~ (>> nth_split E N). Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)