proposition: Lemma Nth_last_inv : forall n x y l, Nth n (l&y) x -> (Nth n l x) \/ (n = length l /\ y = x).
proof: Proof. Proof using. introv H. lets [|(m&E&F)]: Nth_app_inv H. { left~. } { right. inverts F as G. { splits~. math. } { inverts G. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)