Update

thue-morse.v

@@ -1069,6 +1069,24 @@ Proof.
       apply H0.
 Qed.
 
+Lemma tm_step_split_index :
+  forall (k b n m : nat),
+  S k < 2^m -> k = 2^n - 1 + 2^S n * b
+    -> nth_error (tm_step m) k = nth_error (tm_step m) (S k)
+      <-> odd n = true.
+Proof.
+  intros k a b n m. intros H I J.
+  assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
+  apply tm_step_repunit.
+ERREUR DANS l'énoncé : ce n'est pas Some odd mais lié à la parité du poids
+de Hamming de b !!!
+  odd n   XOR    odd Hamming(b)
+     (chaque bit à 1 de b modifie)
+     o
+
+test = lambda b, n: t[ 2**n-1 + 2**(n+1) * b ] == t[ 2**n-1 + 2**(n+1) * b + 1]
+
+