Update

src/thue_morse3.v

@@ -2108,6 +2108,9 @@ Proof.
   assert (K := J).
   rewrite tm_step_palindromic_length_12_prefix
     with (n := n) (hd := hd) (tl := tl) in K.
+  assert (L: even (length hd) = true).
+  rewrite <- Nat.div_exact in K. rewrite K.
+  rewrite Nat.even_mul. reflexivity. easy.
 
   destruct a. inversion I. destruct a. inversion I.
   destruct a. inversion I. destruct a. inversion I.
@@ -2133,6 +2136,15 @@ Proof.
   reflexivity. destruct H1. inversion H1. reflexivity.
   rewrite <- app_assoc. reflexivity. rewrite H0 in H.
 
+  assert (b5 <> b6).
+  replace (hd ++ [b; b0; b1; b2; b3; b5; b5; b6]
+      ++ [b6; b5; b5; b3; b2; b1; b0; b] ++ tl)
+         with ((hd ++ [b; b0; b1; b2; b3]) ++ [b5] ++ [b5] ++ [b6]
+      ++ [b6; b5; b5; b3; b2;b1;b0;b] ++ tl) in H.
+  apply tm_step_cubefree in H. destruct b5; destruct b6.
+  contradiction H. reflexivity. easy. easy. contradiction H. reflexivity.
+  apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
+
   assert (b5 <> b3).
   replace (hd ++ [b; b0; b1; b2; b3; b5; b5; b6]
       ++ [b6; b5; b5; b3; b2; b1; b0; b] ++ tl)
@@ -2142,8 +2154,60 @@ Proof.
   contradiction H. reflexivity. easy. easy. contradiction H. reflexivity.
   apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
 
+  assert (b3 = b6). destruct b3; destruct b5; destruct b6.
+  contradiction H1. reflexivity. contradiction H2. reflexivity.
+  reflexivity. contradiction H1. reflexivity.
+  contradiction H1. reflexivity. reflexivity.
+  contradiction H2. reflexivity. contradiction H1. reflexivity.
+  rewrite H3 in H.
 
+  assert (b0 = b1).
+  replace (hd ++ [b; b0; b1; b2; b6; b5; b5; b6]
+      ++ [b6; b5; b5; b6; b2; b1; b0; b] ++ tl)
+    with ((hd ++ [b]) ++ [b0; b1; b2; b6]
+      ++ [b5; b5; b6; b6; b5; b5; b6; b2; b1; b0; b] ++ tl) in H.
+  assert (length (hd ++ [b]) mod 4 = 1).
+  rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite K.
+  reflexivity. easy.
+  assert (exists x, firstn 2 [b0; b1; b2; b6] = [x; x]).
+  generalize H4.
+  apply tm_step_factor4_1mod4 with (n' := n)
+    (y := [b5; b5; b6; b6; b5; b5; b6; b2; b1; b0; b] ++ tl). assumption.
+  reflexivity. destruct H5. inversion H5. reflexivity.
+  rewrite <- app_assoc. reflexivity. rewrite H4 in H.
 
+  assert ({b2=b6} + {~ b2=b6}). apply bool_dec. destruct H5. rewrite e in H.
+  replace (hd ++ [b; b1; b1; b6; b6; b5; b5; b6]
+      ++ [b6; b5; b5; b6; b6; b1; b1; b] ++ tl)
+    with ((hd ++ [b; b1; b1]) ++ [b6; b6; b5; b5]
+      ++ [b6; b6; b5; b5] ++ [b6; b6; b1; b1; b] ++ tl) in H.
+  assert (even (length ((hd ++ [b; b1; b1]) ++ [b6; b6; b5; b5])) = true).
+  assert (0 < length ([b6; b6; b5; b5])). apply Nat.lt_0_succ.
+  generalize H5. generalize H. apply tm_step_square_pos.
+  rewrite app_length in H5. rewrite app_length in H5.
+  rewrite <- Nat.add_assoc in H5. rewrite Nat.even_add in H5.
+  rewrite L in H5. inversion H5. rewrite <- app_assoc. reflexivity.
+
+  assert (b2 = b5). destruct b2; destruct b6; destruct b5.
+  reflexivity. contradiction n0. reflexivity. reflexivity.
+  contradiction H1. reflexivity. contradiction H1. reflexivity.
+  reflexivity. contradiction n0. reflexivity. reflexivity.
+  rewrite H5 in H.
+
+  assert (b1 <> b5).
+  replace (hd ++ [b; b1; b1; b5; b6; b5; b5; b6]
+      ++ [b6; b5; b5; b6; b5; b1; b1; b] ++ tl)
+    with ((hd ++ [b]) ++ [b1] ++ [b1] ++ [b5]
+      ++ [b6;b5;b5;b6;b6; b5; b5; b6; b5; b1; b1; b] ++ tl) in H.
+  apply tm_step_cubefree in H. destruct b1; destruct b5.
+  contradiction H. reflexivity. easy. easy. contradiction H. reflexivity.
+  apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
+
+  assert (b1 = b6). destruct b1; destruct b5; destruct b6.
+  reflexivity. contradiction H6. reflexivity. reflexivity.
+  contradiction H1. reflexivity. contradiction H1. reflexivity.
+  reflexivity. contradiction H6. reflexivity. reflexivity.
+  rewrite H7 in H.
 
 (*
 Lemma tm_step_proper_palindrome_center :