diff --git a/thue-morse.v b/thue-morse.v
index 282a6d1..ef42fd4 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -831,27 +831,6 @@ Proof.
     reflexivity.
 Qed.
 
-
-Search nth_error.
-(*
-nth_error_None:
-  forall [A : Type] (l : list A) (n : nat),
-  nth_error l n = None <-> length l <= n
-
-nth_error_Some:
-  forall [A : Type] (l : list A) (n : nat),
-  nth_error l n <> None <-> n < length l
- *)
-
-
-(*
-nth_error_split:
-  forall [A : Type] (l : list A) (n : nat) [a : A],
-  nth_error l n = Some a ->
-  exists l1 l2 : list A, l = l1 ++ a :: l2 /\ length l1 = n
- *)
-
-
 Lemma list_app_length_lt : forall (l l1 l2 : list bool) (b : bool),
   l = l1 ++ b :: l2 -> length l1 < length l.
 Proof.