proposition: Lemma nth_pos : forall n x l, n > 0 -> nth n (x::l) = nth (n-1) l.
proof: Proof. Proof using. intros. destruct n. { false. math. } { rewrite nth_succ. fequals. math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)