diff --git a/thue-morse.v b/thue-morse.v
index bcd1371..9a0bf58 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -1265,10 +1265,10 @@ Proof.
   assumption. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. assumption.
 
   apply tm_step_stable. apply lt_split_bits.
-  assumption. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. assumption.
+  assumption. assumption. assumption.
   assert (k*2^m + 2^j < 2^n).
   apply lt_split_bits.
-  assumption. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption. assumption.
+  assumption. assumption. assumption.
   assert (2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.
   generalize H2. generalize H1. apply Nat.lt_le_trans.