From 64d342bbdff3ba90220a142ccd66638fb4a7b7d9 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Tue, 22 Nov 2022 22:45:40 +0100
Subject: [PATCH] Update

---
 thue-morse.v | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/thue-morse.v b/thue-morse.v
index 8d8404f..282a6d1 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -881,7 +881,6 @@ Proof.
 Qed.
 
 
-(*
 Lemma tm_step_next_range :
   forall (n : nat) (l1 l2 : list bool) (b : bool),
   tm_step n = l1 ++ b :: l2
@@ -891,11 +890,11 @@ Proof.
   assert (nth_error (tm_step n) (length l1) = Some b).
   generalize H. apply list_concat_to_pos.
   rewrite tm_build.
-  rewrite nth_error_app1.
- *)
-
-
-
+  assert (I: length l1 < 2^n).
+    rewrite <- tm_size_power2. generalize H. apply list_app_length_lt.
+  rewrite nth_error_app1. apply H0.
+  rewrite tm_size_power2. apply I.
+Qed.
 
 Lemma tm_step_next_range2 :
   forall (n : nat) (l1 l2 : list bool) (b : bool),
@@ -909,6 +908,11 @@ Proof.
   assert (I: length l1 < 2^n).
     rewrite <- tm_size_power2. generalize H. apply list_app_length_lt.
   rewrite nth_error_app2. rewrite tm_size_power2.
+  replace (length l1 + 2^n - 2^n) with (length l1).
+  apply map_nth_error. apply H0.
+  rewrite Nat.add_sub. reflexivity.
+  rewrite tm_size_power2. apply Nat.le_add_l.
+Qed.