diff --git a/thue-morse.v b/thue-morse.v
index 1519df9..a54b476 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -1338,7 +1338,7 @@ Qed.
 
 
 
-Lemma tm_step_add_small_power :
+Lemma 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).
@@ -1407,21 +1407,6 @@ Qed.
 
 
 
-Lemma greedy_power2 : forall (n m : nat),
-  0 < n -> n = 2^(Nat.log2 n) + m -> m < 2^(Nat.log2 n).
-Proof.
-  intros n m. intros H I.
-  rewrite Nat.add_lt_mono_l with (p := 2^(Nat.log2 n)).
-  rewrite <- I.
-  replace (2^(Nat.log2 n) + 2^(Nat.log2 n)) with (2* (2^(Nat.log2 n))).
-  rewrite <- Nat.pow_succ_r.
-  apply Nat.log2_spec. apply H. apply Nat.log2_nonneg.
-  simpl. rewrite Nat.add_0_r. reflexivity.
-Qed.
-
-
-
-