proposition: Lemma Nth_rev : forall n x l, Nth n l x -> Nth (length l - 1 - n) (rev l) x.
proof: Proof. Proof using. introv. sets_eq N: (length l). gen x n l. induction N; introv E I; destruct l; tryfalse. { inverts I. } { rewrite rev_cons. inverts I as I. { applys Nth_app_r' 0. { constructors. } { rewrite length_rev. rewrite length_cons in E. math. } } { rew_list in E. lets K: IHN I. { math. } apply Nth_app_l. applys_eq K. math. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)