proposition: Lemma nth_error_nth : forall (l : list A) (n : nat) (x d : A), nth_error l n = Some x -> nth n l d = x.
proof: Proof. intros l n x d H. apply nth_error_split in H. destruct H as [l1 [l2 [H H']]]. subst. rewrite app_nth2; [|auto]. rewrite Nat.sub_diag. reflexivity. Qed.
imports: PeanoNat