diff --git a/thue-morse.v b/thue-morse.v
index ef3cbd0..1a66351 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -946,20 +946,15 @@ Proof.
   intros n k. intros H.
   rewrite tm_build.
   rewrite nth_error_app2. rewrite tm_size_power2. rewrite Nat.add_sub.
-
   assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
   generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
   rewrite H0.
-
-  assert (nth_error (map negb (tm_step n)) k =
-    Some (negb (nth k (tm_step n) false))).
-    generalize H0. apply map_nth_error.
-    rewrite H1.
-
-  
-    destruct (nth_error (tm_step n) k). rewrite <- H0. rewrite <- H0.
-
-
+  assert (nth_error (map negb (tm_step n)) k
+    = Some (negb (nth k (tm_step n) false))).
+  generalize H0. apply map_nth_error. rewrite H1.
+  destruct (nth k (tm_step n) false). easy. easy.
+  rewrite tm_size_power2. apply Nat.le_add_l.
+Qed.