From 0fe7e6dd25a85ac51281b5b70c7b6097fbd844c5 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Sun, 22 Jan 2023 22:36:48 +0100
Subject: [PATCH] Update

---
 src/thue_morse3.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 21166ec..d398bb4 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -582,6 +582,8 @@ Proof.
   apply tm_step_cubefree in H. contradiction H. reflexivity.
   apply Nat.lt_0_succ. reflexivity. easy. easy.
 
+  assert (H' := H).
+
   (* SECOND PART PF THE PROOF: case b0 <> b1 *)
   (* sinon, sur la base de    T F T F || F T F T
         quatre cas :
@@ -956,6 +958,14 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   rewrite <- Nat.add_assoc. replace (2+8) with 10.
   replace (8) with (2^3) at 1. rewrite <- Nat.pow_add_r.
   rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. simpl.
+  rewrite <- tm_size_power2. rewrite H'. unfold lh.
+  rewrite app_length. rewrite app_length. rewrite <- Nat.add_assoc.
+  rewrite <- Nat.add_lt_mono_l. simpl.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  apply Nat.lt_0_succ. apply Nat.le_refl.
+  apply Nat.lt_le_incl. assumption. reflexivity. reflexivity.
+  assumption. apply Nat.lt_0_succ.