Update

src/thue_morse.v

@@ -1344,15 +1344,3 @@ Proof.
     apply Nat.lt_irrefl in H2. contradiction H2.
   - assumption.
 Qed.
-
-
-
-
-
-
-
-(**
-   Under construction
-*)
-
-

src/thue_morse2.v

@@ -0,0 +1,41 @@
+Require Import thue_morse.
+
+Require Import Coq.Lists.List.
+Require Import PeanoNat.
+Require Import Nat.
+Require Import Bool.
+
+Import ListNotations.
+
+
+
+
+
+
+
+
+(**
+   Under construction
+*)
+
+Lemma xxx : forall (n k : nat) (hd pat tl : list bool),
+  tm_step n = hd ++ pat ++ tl
+  -> length pat <= 2^k
+  -> exists (hd2 tl2 : list bool),
+       tm_step (S k) = hd2 ++ pat ++ tl2 /\ length (hd2 ++ pat) < 3 * (2^k).
+Proof.
+  intros n k hd pat tl. intros H I.
+
+
+
+
+L'inégalité finale doit être stricte, car si le motif fait exactement 2^k
+et se situe à la fin des 3 * (2^k) termes, il est aussi au début !
+
+Lemma tm_step_repeating_patterns :
+  forall (n m i j : nat),
+  i < 2^m -> j < 2^m
+  -> forall k, k < 2^n -> nth_error (tm_step m) i
+                        = nth_error (tm_step m) j
+                      <-> nth_error (tm_step (m+n)) (k * 2^m + i)
+                        = nth_error (tm_step (m+n)) (k * 2^m + j).