proposition: Lemma Nth_combine : forall A B n (r:list A) (s:list B) x y, Nth n r x -> Nth n s y -> Nth n (combine r s) (x,y).
proof: Proof. Proof using. introv N1. gen s. induction N1; introv N2; inverts N2. { constructors. } { rewrite combine_cons. constructors~. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)