diff --git a/thue-morse.v b/thue-morse.v
index 9da7180..cd4cfba 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -1100,7 +1100,7 @@ Proof.
   assert (2^n < 2^(S n)). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
   apply Nat.lt_succ_diag_r.
   generalize H1. generalize H0. apply Nat.lt_trans. rewrite <- H1.
-  rewrite tm_step_repunit_index.
+  rewrite tm_step_repunit_index. destruct (odd n). easy. easy.
 
   rewrite Nat.succ_lt_mono. simpl.
   (*