Update

src/thue_morse2.v

@@ -1535,18 +1535,6 @@ Proof.
   assert (K: even (length a') = true).
   rewrite <- Nat.negb_odd. rewrite n0. reflexivity.
 
-  (*
-  assert (L: even (length (hd ++ a')) = true).
-  rewrite Nat.le_succ_l in J. apply Nat.lt_succ_l in J.
-  apply Nat.lt_succ_l in J. apply Nat.lt_succ_l in J.
-  generalize J. generalize H. apply tm_step_square_pos.
-
-  assert (M: even (length hd) = true).
-  rewrite app_length in L. rewrite Nat.even_add_even in L.
-  assumption.
-  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
-  *)
-
   assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
   destruct W. rewrite e in H. right.
   destruct n. inversion H. rewrite app_nil_l in H.
@@ -1634,3 +1622,31 @@ Proof.
   simpl. rewrite Nat.add_0_r. reflexivity.
   left. assumption.
 Qed.
+
+Theorem tm_step_square_prefix_not_nil :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl -> 0 < length a -> hd <> nil.
+Proof.
+  intros n hd a tl. intros H I.
+
+  assert (W: {hd=nil} + {~ hd=nil}). apply list_eq_dec. apply bool_dec.
+  destruct W. rewrite e in H. rewrite app_nil_l in H.
+  generalize dependent a.
+  generalize dependent tl.
+  induction n.
+  - intros tl a. intros H I.
+    destruct a. inversion I. inversion H.
+    assert (length (nil : list bool) = length (nil : list bool)).
+    reflexivity. rewrite H2 in H0 at 2. rewrite app_length in H0.
+    rewrite Nat.add_comm in H0. inversion H0.
+  - intros tl a. intros H I.
+    assert (hd <> nil
+      \/ exists a' tl', tm_step (pred (S n)) = a' ++ a' ++ tl' /\ 0 < length a').
+    generalize I. generalize H. replace (a++a++tl) with (hd ++ a ++ a ++ tl).
+    apply tm_step_square_prefix_not_nil0. rewrite e. reflexivity.
+    destruct H0. assumption. destruct H0. destruct H0.
+    rewrite <- pred_Sn in H0.
+    destruct H0.
+    generalize H1. generalize H0. apply IHn.
+  - assumption.
+Qed.