diff --git a/thue-morse.v b/thue-morse.v
index 3550dd0..497aca2 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -859,7 +859,6 @@ Proof.
   rewrite nth_middle in L. apply L. rewrite H. reflexivity.
 Qed.
 
-
 Lemma tm_step_next_range :
   forall (n : nat) (l1 l2 : list bool) (b : bool),
   tm_step n = l1 ++ b :: l2
@@ -869,12 +868,25 @@ Proof.
   assert (nth_error (tm_step n) (length l1) = Some b).
   generalize H. apply list_concat_to_pos.
   rewrite tm_build.
-  assert (I: length l1 < 2^n).
-    rewrite <- tm_size_power2. generalize H. apply list_app_length_lt.
-  rewrite nth_error_app1. apply H0.
-  rewrite tm_size_power2. apply I.
+  assert (length l1 < length (tm_step n)).
+    generalize H. apply list_app_length_lt.
+  rewrite nth_error_app1. apply H0. apply H1.
 Qed.
 
+Lemma tm_step_next_range' :
+  forall (n k : nat) (l1 l2 : list bool) (b : bool),
+  tm_step n = l1 ++ b :: l2
+  -> nth_error (tm_step (n + k)) (length l1) = Some b.
+Proof.
+  intros n k l1 l2 b. intros H.
+  induction k.
+  - rewrite Nat.add_0_r. generalize H. apply list_concat_to_pos.
+  - rewrite Nat.add_succ_r. 
+    simpl.
+    apply nth_error_split in IHk.
+
+
+
 Lemma tm_step_next_range2 :
   forall (n : nat) (l1 l2 : list bool) (b : bool),
   tm_step n = l1 ++ b :: l2