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