From 77c78b24d531cf818764fe4c50fc1bc2332a269c Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Wed, 8 Feb 2023 22:02:43 +0100
Subject: [PATCH] Update

---
 src/thue_morse4.v | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/thue_morse4.v b/src/thue_morse4.v
index f93f223..729be8a 100644
--- a/src/thue_morse4.v
+++ b/src/thue_morse4.v
@@ -168,7 +168,10 @@ Lemma xxx :
   tm_step n = hd ++ a ++ a ++ tl
   -> a = rev a
   -> 0 < length a
-  -> length a <= 4 \/ 11 = 42 \/ 17 = 55.
+  -> length a <= 4
+    \/ (exists m, length a = 2 ^ m /\
+        length (hd ++ a) mod 2 ^ pred (Nat.double (Nat.div2 (S m))) = 0)
+    \/ length a = 3 * 2^(pred (Nat.log2 (length a))).
 Proof.
   intros n hd a tl. intros H I J.
   destruct n. assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
@@ -197,4 +200,8 @@ Proof.
     assert (length (hd ++ a) mod 2^(pred (Nat.double (Nat.div2 (S x0)))) = 0).
     generalize H3. generalize H0. generalize H.
     apply tm_step_palindrome_power2.
-
+    right. left. exists x0. split; assumption.
+  - right. right. rewrite H0. rewrite Nat.mul_cancel_l.
+    rewrite Nat.log2_mul_pow2. rewrite Nat.add_1_r.
+    rewrite Nat.pred_succ. reflexivity. lia. lia. lia.
+Qed.