proposition: Lemma Nth_rev_inv : forall n x l, Nth n (rev l) x -> Nth (length l - 1 - n) l x.
proof: Proof. Proof using. introv N. lets K: Nth_rev N. rewrite rev_rev, length_rev in K. auto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)