diff --git a/thue-morse.v b/thue-morse.v
index 3b54198..ef3cbd0 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -939,6 +939,34 @@ Proof.
   rewrite tm_size_power2. apply Nat.le_add_l.
 Qed.
 
+Lemma tm_step_next_range2'' :
+  forall (n k : nat),
+  k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n).
+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.
+
+
+
+
+
+
+
+
+
 Lemma tm_step_next_range2_neighbor : forall (n k : nat),
   S k < 2^n ->
     eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false)