Update

src/thue_morse3.v

@@ -2535,7 +2535,26 @@ Proof.
 Qed.
 
 
+Lemma tm_step_palindromic_power2_odd_beta :
+  forall (m n : nat) (hd a tl : list bool),
+    tm_step n = hd ++ a ++ (rev a) ++ tl
+    -> 6 < length a
+    -> length a = 2^(S (Nat.double m))
+    -> length (hd ++ a) mod (2 ^ (S (Nat.double m))) = 0
+       \/ 2^5 <= length a.
+Proof.
+  intros m n hd a tl. intros H I J.
 
+  destruct m. rewrite J in I. inversion I. inversion H1. inversion H3.
+
+  destruct m. left.
+  apply tm_step_palindrome_mod8 with (n := n) (tl := tl); assumption.
+  right. rewrite J. apply Nat.pow_le_mono_r. easy.
+  rewrite Nat.double_S. rewrite Nat.double_S.
+  rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
+  rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
+  rewrite <- Nat.succ_le_mono. apply le_0_n.
+Qed.
 
 
 (*