proposition: Lemma nth_combine : forall `{IA:Inhab A} `{IB:Inhab B} n (r:list A) (s:list B), n < length r -> length r = length s -> nth n (combine r s) = (nth n r, nth n s).
proof: Proof. Proof using. introv N E. applys nth_of_Nth. applys* Nth_combine. { applys* Nth_nth. } { applys* Nth_nth. math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)