From 3c2f4121e13d5e4f7fb4d1c708577255d90374ee Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Sat, 14 Jan 2023 21:03:04 +0100
Subject: [PATCH] Update

---
 src/thue_morse.v  | 2 +-
 src/thue_morse2.v | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/thue_morse.v b/src/thue_morse.v
index 4c4e824..98ae8a0 100644
--- a/src/thue_morse.v
+++ b/src/thue_morse.v
@@ -413,7 +413,7 @@ Proof.
     apply tm_step_count_occ.
     rewrite count_occ_app in L. rewrite count_occ_app in L.
     rewrite K in L. rewrite Nat.add_cancel_l in L.
-    destruct b; simpl in L; inversion L.
+    destruct b; inversion L.
 Qed.
 
 Lemma tm_step_consecutive_identical' :
diff --git a/src/thue_morse2.v b/src/thue_morse2.v
index 92b74d4..3ff4cec 100644
--- a/src/thue_morse2.v
+++ b/src/thue_morse2.v
@@ -515,5 +515,7 @@ Proof.
 
     (* TODO: utiliser tm_step_odd_prefix_square pour le cas impair *)
     (* TODO: la taille du facteur divise la taille du préfixe ? *)
+    (* TODO : le cas de la taille 2 est un cas pair facile
+       grâce à tm_step_factor4_odd_prefix *)
 
- 
+    Admitted.