Update

src/thue_morse3.v

@@ -2669,6 +2669,45 @@ Proof.
 Qed.
 
 
+Theorem tm_step_palindrome_power2 :
+  forall (m n : nat) (hd a tl : list bool),
+    tm_step n = hd ++ a ++ (rev a) ++ tl
+    -> length a = 2^m
+    -> 2 < m
+    -> length (hd ++ a) mod 2^ (pred (Nat.double (Nat.div2 (S m)))) = 0.
+Proof.
+  intros m n hd a tl. intros H I J.
+
+  assert (L: 6 < length a). rewrite I.
+  assert (2^3 <= 2^m). apply Nat.pow_le_mono_r_iff.
+  apply Nat.lt_1_2. rewrite Nat.le_succ_l. assumption.
+  assert (6 < 2^3). simpl.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  apply Nat.lt_0_2.
+  generalize H0. generalize H1. apply Nat.lt_le_trans.
+
+  assert (E: Nat.Even m \/ Nat.Odd m). apply Nat.Even_or_Odd.
+  destruct E as [E|E].
+
+  assert (E' := E). rewrite <- Nat.Odd_succ in E.
+  apply Nat.Even_Odd_double in E.
+  apply eq_add_S in E. apply f_equal_pred in E.
+  rewrite <- E.
+  apply Nat.Even_Odd_double in E'. rewrite E'.
+  apply tm_step_palindromic_power2_even with (n := n) (tl := tl).
+  assumption. assumption. rewrite <- E'. assumption.
+
+  assert (E' := E). rewrite <- Nat.Even_succ in E.
+  apply Nat.Even_Odd_double in E.
+  apply f_equal_pred in E. rewrite <- pred_Sn in E.
+  rewrite <- E.
+  apply Nat.Even_Odd_double in E'. rewrite E'.
+  apply tm_step_palindromic_power2_odd with (n := n) (tl := tl).
+  assumption. assumption. rewrite <- E'. assumption.
+Qed.
+
 
 (*
 Lemma tm_step_proper_palindrome_center :