diff --git a/thue-morse.v b/thue-morse.v
index d22196b..162ed78 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -681,11 +681,14 @@ Proof.
   apply Nat.mul_pos_pos. apply Nat.lt_0_succ.
   assumption.
 
+  assert(T: S (2 * k) * 2 ^ m - 1 < 2 ^ n0).
+  generalize I. generalize L. apply Nat.lt_trans.
+
   assert (nth_error (tm_step n0) ((S (2 * k) * 2 ^ m) - 1)
     <> nth_error (tm_step (S n0)) (S (2 * (S (2 * k) * 2 ^ m - 1)))).
   apply tm_step_succ_double_index.
 
-  generalize I. generalize L. apply Nat.lt_trans.
+  assumption.
 
   replace (S (2 * (S (2 * k) * 2 ^ m - 1))) with (2 * (S (2*k) * 2^m) - 1) in H.
   rewrite Nat.odd_succ. rewrite <- Nat.negb_odd. destruct (odd m).
@@ -728,8 +731,8 @@ Proof.
   simpl; split; reflexivity.
 
   assumption. rewrite tm_size_power2. assumption. assumption.
-  rewrite tm_size_power2. generalize I. generalize L. apply Nat.lt_trans.
-  rewrite tm_size_power2. generalize I. generalize L. apply Nat.lt_trans.
+  rewrite tm_size_power2. assumption.
+  rewrite tm_size_power2. assumption.
   rewrite tm_size_power2. assumption.
 
   rewrite Nat.mul_sub_distr_l. rewrite Nat.mul_1_r.