diff --git a/thue-morse.v b/thue-morse.v
index a1a68f6..0de2121 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -1335,10 +1335,7 @@ Proof.
       rewrite tm_size_power2. assumption.
 Qed.
 
-
-
-
-Lemma tm_step_flip_low_bit :
+Theorem tm_step_flip_low_bit :
   forall (n m k j : nat),
   0 < k -> j < m -> k * 2^m < 2^n
   -> nth_error (tm_step n) (k * 2^m) <> nth_error (tm_step n) (k * 2^m + 2^j).