diff --git a/thue-morse.v b/thue-morse.v
index cd4cfba..9800b77 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -1102,7 +1102,6 @@ Proof.
   generalize H1. generalize H0. apply Nat.lt_trans. rewrite <- H1.
   rewrite tm_step_repunit_index. destruct (odd n). easy. easy.
 
-  rewrite Nat.succ_lt_mono. simpl.
   (*
   assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
   apply tm_step_repunit.