From c2b3b67b87d349ab077250735c9cedb48a3e8c6f Mon Sep 17 00:00:00 2001
From: Thomas Baruchel <baruchel@gmx.com>
Date: Sat, 26 Nov 2022 20:33:13 +0100
Subject: [PATCH] Update

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

diff --git a/thue-morse.v b/thue-morse.v
index 3b018c9..2eca326 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -1106,10 +1106,67 @@ Proof.
   rewrite tm_step_repunit_index. destruct (odd n). easy. easy.
   rewrite <- J. rewrite I.
 
+
+  induction k.
+  - rewrite <- I.
+    assert (b=0).
+    { symmetry in I. rewrite Nat.eq_add_0 in I. destruct I.
+      apply Nat.mul_eq_0_r in H1. apply H1. apply Nat.pow_nonzero.
+      easy. }
+    rewrite H0 in I. rewrite Nat.mul_0_r in I.
+    rewrite Nat.add_0_r in I. rewrite <- I.
+
+    replace (2^n) with (S (2^n - 1)). rewrite <- I.
+
+    split.
+
+    intros. rewrite tm_step_head_2 at 2. rewrite tm_step_head_1. simpl.
+    replace (m) with (S (m-1)) in H1 at 2.
+    rewrite tm_step_head_2 in H1. rewrite tm_step_head_1 in H1. simpl in H1.
+    apply H1.
+    destruct m. simpl in H. apply Nat.lt_irrefl in H. contradiction H.
+    rewrite Nat.sub_1_r. simpl. reflexivity.
+
+    intros. rewrite tm_step_head_2 in H1 at 2.
+    rewrite tm_step_head_1 in H1. simpl in H1. inversion H1.
+    rewrite <- I.
+    apply eq_S in I. rewrite I at 1.
+    apply Nat.pred_inj. apply Nat.neq_succ_0. apply Nat.pow_nonzero.
+    easy. simpl. rewrite Nat.sub_1_r. reflexivity.
+
+  -
+
+
+
+
+    split. intros. apply H1.
+
+
+
+
+
+
+
+
+    assert (K: S (2 ^ n - 1 + 2 ^ S n * b) = (2 ^ n + 2 ^ S n * b)).
+    + rewrite Nat.sub_1_r. rewrite <- Nat.add_succ_l.
+      rewrite Nat.succ_pred_pos. reflexivity.
+      rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+    + rewrite K. symmetry.
+      split. intros. symmetry.
+      apply tm_step_add_range2_flip_two.
+
+
   (*
   assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
   apply tm_step_repunit.
    *)
+Lemma tm_step_add_range2_flip_two : forall (n m j k : nat),
+  k < 2^n -> m < 2^n ->
+    nth_error (tm_step n) k = nth_error (tm_step n) m
+    <->
+    nth_error (tm_step (S n+j)) (k + 2^(n+j))
+      = nth_error (tm_step (S n+j)) (m + 2^(n+j)).
   
 
 
@@ -1117,6 +1174,12 @@ Proof.
 
 
 
+Déclagae vers la droite de k zéros pour un Bins :
+Pos.iter xO xH 3.   (ici k = 3)
+  --> on ajoute 3 zéros à gauche
+
+
+
 
 
 
@@ -1161,12 +1224,6 @@ Admitted.
 
 
 
-Déclagae vers la droite de k zéros pour un Bins :
-Pos.iter xO xH 3.   (ici k = 3)
-  --> on ajoute 3 zéros à gauche
-
-
-
 
 Theorem tm_step_consecutive : forall (n : nat) (l1 l2 : list bool) (b1 b2 : bool),
   tm_step n = l1 ++ b1 :: b2 :: l2 ->