diff --git a/thue-morse.v b/thue-morse.v
index ce11f30..10e950a 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -890,10 +890,20 @@ Proof.
   rewrite tm_size_power2. apply Nat.le_add_l.
 Qed.
 
-
-
-
-
+Lemma tm_step_next_range2' :
+  forall (n k : nat) (b : bool),
+  nth_error (tm_step n) k = Some b
+    -> nth_error (tm_step (S n)) (k + 2^n) = Some (negb b).
+Proof.
+  intros n k b. intros H. assert (I := H).
+  apply nth_error_split in H. destruct H. destruct H. inversion H.
+  rewrite tm_build.
+  assert (J: k < 2^n).
+  rewrite <- tm_size_power2. rewrite <- H1. generalize H0. apply list_app_length_lt.
+  rewrite nth_error_app2. rewrite tm_size_power2.
+  rewrite Nat.add_sub. apply map_nth_error. apply I.
+  rewrite tm_size_power2. apply Nat.le_add_l.
+Qed.
 
 
 Lemma tm_step_consecutive_power2 :