proposition: Lemma Nth_inbound_inv : forall n l, n < length l -> exists x, Nth n l x.
proof: Proof. Proof using. induction n; introv N; destruct l as [|a l']; rew_list in N; try solve [math]. { eauto. } { simpls. forwards (x&Hx): IHn l'. math. exists x. apply* Nth_succ. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)