From bb3687969ee4eddf1806654f9f07a77d2dcb28f0 Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Sat, 10 Dec 2022 21:31:26 +0100
Subject: [PATCH] Update

---
 thue-morse.v | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

diff --git a/thue-morse.v b/thue-morse.v
index 9392fb2..4909f65 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -769,20 +769,13 @@ Proof.
     reflexivity.
 Qed.
 
-Lemma tm_size_double : forall n : nat,
-  length (tm_step (S n)) = length (tm_step n) + length (tm_step n).
-Proof.
-  intros n. rewrite tm_build. rewrite app_length. rewrite map_length.
-  reflexivity.
-Qed.
-
 Theorem tm_size_power2 : forall n : nat, length (tm_step n) = 2^n.
 Proof.
   intros n.
   induction n.
   - reflexivity.
-  - rewrite tm_size_double. replace (2^S n) with (2^n + 2^n).
-    rewrite IHn. reflexivity.
+  - rewrite tm_build. rewrite app_length. rewrite map_length.
+    replace (2^S n) with (2^n + 2^n). rewrite IHn. reflexivity.
     simpl. rewrite <- plus_n_O. reflexivity.
 Qed.
 
@@ -1262,14 +1255,20 @@ Proof.
   generalize H1. generalize I. apply Nat.lt_le_trans.
 Qed.
 
+(* vérifier si les deux sont nécessaires *)
+Require Import BinPosDef.
+Require Import BinPos.
 
-
+Theorem tm_step_double_index : forall (p : positive),
+  nth_error (tm_step (Pos.size_nat p)) (Pos.to_nat p)
+  = nth_error (tm_step (S (Pos.size_nat p))) (Pos.to_nat (xO p)).
+Proof.
+  intros p.
+  induction p.
 
 
 
 Require Import BinNat.
-Require Import BinPosDef.
-Require Import BinPos.