diff --git a/thue-morse.v b/thue-morse.v
index bb4a54b..9d9b1e4 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -615,19 +615,16 @@ Proof.
 Qed.
 
 Lemma tm_step_succ_double_index : forall (n k : nat),
-  2 * k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step n) (S (2*k)).
+  k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (S (2*k)).
 Proof.
   intros n k. intro H. rewrite tm_step_double_index.
-  replace (nth_error (tm_step (S n)) (2*k)) with (nth_error (tm_step n) (2*k)).
   rewrite Nat.mul_comm. replace (2) with (2^1).
   replace (S (k*2^1)) with (k*2^1 + 2^0).
   apply tm_step_flip_low_bit. apply Nat.lt_0_1.
-  simpl. rewrite Nat.mul_comm. assumption.
-  rewrite Nat.add_1_r. reflexivity. easy.
-  apply tm_step_stable. assumption.
-  assert (2^n < 2^(S n)). apply Nat.pow_lt_mono_r.
-  apply Nat.lt_1_2. apply Nat.lt_succ_diag_r.
-  generalize H0. generalize H. apply Nat.lt_trans.
+  simpl. rewrite Nat.add_0_r. replace (k*2) with (k+k).
+  apply Nat.add_lt_mono; assumption.
+  rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
+  simpl. rewrite Nat.add_1_r. reflexivity. reflexivity.
 Qed.