Update

src/thue_morse2.v

@@ -207,7 +207,7 @@ Proof.
 Qed.
 
 
-Lemma two_step_consecutive_identical_length :
+Lemma tm_step_consecutive_identical_length :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ tl -> length a = 5
   -> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c.
@@ -261,10 +261,39 @@ Proof.
   exists (nil). exists (false::false::false::nil). exists false. simpl. reflexivity.
 Qed.
 
+Lemma tm_step_consecutive_identical_length' :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ tl -> length a > 4
+  -> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c.
+Proof.
+  intros n hd a tl. intros H I.
+  rewrite <- firstn_skipn with (l := a) (n := 5).
+  assert (length (firstn 5 a) = 5).
+  apply firstn_length_le. apply Nat.le_succ_l. apply I.
+  rewrite <- firstn_skipn with (l := a) (n := 5) in H.
+  rewrite <- app_assoc in H.
+  assert (exists (b1 c1 : list bool) (d1 : bool),
+    firstn 5 a = b1 ++ [d1; d1] ++ c1).
+  generalize H0. generalize H. apply tm_step_consecutive_identical_length.
+  destruct H1. destruct H1. destruct H1. rewrite H1.
+  exists x. exists (x0 ++ (skipn 5 a)). exists x1.
+  rewrite <- app_assoc. apply app_inv_head_iff.
+  rewrite <- app_assoc. reflexivity.
+Qed.
 
 
 
 
+
+
+
+Lemma tm_step_consecutive_identical_length :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ tl -> length a = 5
+  -> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c.
+
+
+
 Lemma tm_step_square_size_3 : forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ a ++ tl -> length a = 3
   -> a = true::false::true::nil \/ a = false::true::false::nil.