Update

src/thue_morse3.v

@@ -2233,6 +2233,29 @@ Proof.
   rewrite <- Nat.le_succ_l. apply Nat.le_succ_diag_r.
 Qed.
 
+
+Lemma tm_step_palindrome_8_mod8 :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ (rev a) ++ tl
+  -> length a = 8
+  -> length (hd ++ a) mod 8 = 0.
+Proof.
+  intros n hd a tl. intros H I.
+
+  assert (J: length a mod 4 = 0). rewrite I. reflexivity.
+  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.
+
+  assert (M: exists x, a = [x; negb x; negb x; x; negb x; x; x; negb x]).
+  generalize I. generalize H. apply tm_step_palindrome_8_destruct.
+  destruct M as [x M].
+
+
+
 (*
 Lemma tm_step_proper_palindrome_center :
   forall (m n k : nat) (hd a tl : list bool),