Update

thue-morse.v

@@ -1069,15 +1069,18 @@ Proof.
       apply H0.
 Qed.
 
-Lemma tm_step_split_index :
+Lemma tm_step_cancel_high_bits :
   forall (k b n m : nat),
+  (* every natral number k can be written according to the following form *)
   S k < 2^m -> k = 2^n - 1 + 2^S n * b
     -> nth_error (tm_step m) k = nth_error (tm_step m) (S k)
       <-> odd n = true.
 Proof.
-  intros k a b n m. intros H I J.
+  intros k b n m. intros H I.
+  (*
   assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
   apply tm_step_repunit.
+   *)