From 8f1fd646dbfb2dfa899c43d0353f68b803d492c4 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Mon, 13 Feb 2023 06:18:37 +0100
Subject: [PATCH] Update

---
 src/thue_morse4.v | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/thue_morse4.v b/src/thue_morse4.v
index c64ad4f..545770a 100644
--- a/src/thue_morse4.v
+++ b/src/thue_morse4.v
@@ -1559,7 +1559,7 @@ Proof.
   apply tm_step_square_rev_even.
 Qed.
 
-Lemma tm_step_square2_even_pos :
+Lemma tm_step_square2_rev_even' :
   forall (m n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ a ++ tl
   -> length a = 2^m
@@ -1756,3 +1756,17 @@ Proof.
   rewrite <- Nat.add_sub_assoc. rewrite <- Nat.mul_sub_distr_r.
   apply Nat.le_add_r. apply Nat.mul_le_mono_r. lia. lia.
 Qed.
+
+Lemma tm_step_square3_rev_even' :
+  forall (m n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ a ++ tl
+  -> length a = 3 * 2^m
+  ->  even m = true
+  -> length (hd ++ a) mod 2^(S m) = 0.
+Proof.
+  intros m n hd a tl. intros H I J.
+  assert (a = rev a).
+  rewrite tm_step_square3_rev_even_swap
+    with (n := n) (hd := hd) (a := a) (tl := tl) (m := m) in J; assumption.
+  generalize H0. generalize I. generalize H. apply tm_step_square3_rev_even.
+Qed.