diff --git a/thue-morse.v b/thue-morse.v
index ebfcc62..1ca36f9 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -1231,6 +1231,7 @@ Proof.
 
   assert (O: k*2^m + 2^j < 2^n).
   apply lt_split_bits. assumption. assumption. assumption.
+  assert (P: 2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.
 
   assert ( nth_error (tm_step m) 0
          = nth_error (tm_step m) (2^j)
@@ -1265,14 +1266,12 @@ Proof.
   apply H1 in H2. rewrite H2 at 1. easy. easy.
   rewrite nth_error_nth' with (d := false). easy.
   rewrite tm_size_power2. assumption.
-  apply tm_step_stable. assumption.
-
-  assert (2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.
-  generalize H1. generalize O. apply Nat.lt_le_trans.
 
   apply tm_step_stable. assumption.
-  assert (2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.
-  generalize H1. generalize I. apply Nat.lt_le_trans.
+  generalize P. generalize O. apply Nat.lt_le_trans.
+
+  apply tm_step_stable. assumption.
+  generalize P. generalize I. apply Nat.lt_le_trans.
 Qed.