Add some minor results about single-step behavior of nth_error

theories/Lists/List.v

@@ -615,6 +615,34 @@ Section Elts.
       intro n. exact (Hnth (S n)).
   Qed.
 
+  Lemma nth_error_match l n
+    : nth_error l n
+      = match n, l with
+        | O, x :: _ => Some x
+        | S n, _ :: l => nth_error l n
+        | _, _ => None
+        end.
+  Proof using Type. destruct n; reflexivity. Qed.
+
+  Lemma nth_error_nil n : nth_error nil n = None.
+  Proof using Type. destruct n; reflexivity. Qed.
+
+  Lemma nth_error_cons x xs n
+    : nth_error (x :: xs) n
+      = match n with
+        | O => Some x
+        | S n => nth_error xs n
+        end.
+  Proof using Type. apply nth_error_match. Qed.
+
+  Lemma nth_error_O l
+    : nth_error l O = hd_error l.
+  Proof using Type. destruct l; reflexivity. Qed.
+
+  Lemma nth_error_S l n
+    : nth_error l (S n) = nth_error (tl l) n.
+  Proof using Type. destruct l; rewrite ?nth_error_nil; reflexivity. Qed.
+
   (** Results directly relating [nth] and [nth_error] *)
 
   Lemma nth_error_nth : forall (l : list A) (n : nat) (x d : A),