Update

src/thue_morse3.v

@@ -1912,21 +1912,21 @@ Proof.
 
   induction m.
   - assert (even (length (hd' ++ a')) = true).
+    assert (0 < length a'). rewrite J in N.
+    replace (2 ^ (Nat.double 2)) with (4*4) in N.
+    rewrite Nat.mul_cancel_l in N. rewrite <- N.
+    apply Nat.lt_0_succ. easy. reflexivity. generalize H0.
+    generalize H. apply tm_step_palindromic_even_center.
+
+    replace (2^pred (Nat.double 2)) with (4*2).
+    replace (length (hd ++ a)) with (4 * length (hd' ++ a')).
+    rewrite Nat.mul_mod_distr_l. rewrite Nat.mul_eq_0. right.
 
 
 
 
 
 
-Theorem tm_step_palindromic_even_center :
-  forall (n : nat) (hd a tl : list bool),
-  tm_step n = hd ++ a ++ (rev a) ++ tl
-  -> 0 < length a
-  -> even (length (hd ++ a)) = true.
-
-
-
-
 
 
 Lemma tm_step_proper_palindrome_center :