Update

src/thue_morse3.v

@@ -1860,6 +1860,37 @@ Qed.
 
 
 
+Lemma tm_step_proper_palindrome_center :
+  forall (m n k : nat) (hd a tl : list bool),
+    tm_step n = hd ++ a ++ (rev a) ++ tl
+    -> 6 < length a
+    -> length a = 2^(Nat.double m)     (* palindrome non propre *)
+    -> skipn (length hd - length a) hd = rev (firstn (length a) tl).
+Proof.
+  intros m n k hd a tl. intros H I J.
+
+  assert (W: (length a) mod 4 = 0). rewrite J in I.
+  destruct m. inversion I. inversion H1.
+  destruct m. inversion I. inversion H1.
+  inversion H3. inversion H5. inversion H7.
+  rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J.
+  rewrite Nat.double_S in J. rewrite Nat.pow_succ_r in J.
+  rewrite Nat.mul_assoc in J.
+  replace (2*2) with 4 in J. rewrite J.
+  rewrite <- Nat.mul_mod_idemp_l. reflexivity.
+  easy. reflexivity. apply le_0_n. apply le_0_n.
+
+  assert (
+     hd = tm_morphism (tm_morphism (firstn (length hd / 4)
+           (tm_step (pred (pred n)))))
+     /\ a = tm_morphism (tm_morphism
+           (firstn (length a / 4) (skipn (length hd / 4)
+           (tm_step (pred (pred n))))))
+     /\ tl = tm_morphism (tm_morphism
+           (skipn (length hd / 4 + Nat.div2 (length a))
+             (tm_step (pred (pred n)))))).
+  generalize W. generalize I. generalize H.
+  apply tm_step_palindromic_even_morphism2.