diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 42df08b..d1ef92b 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -860,7 +860,12 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   rewrite e0 in H7. inversion H7. assumption.
   easy.
 
-(* TODO : prouver le très important 8 <= lh *)
+  assert (T: 8 <= length ((b3 :: b5 :: b7 :: hd) ++ [b; b0; b1; b2])).
+  destruct hd. inversion Q. rewrite app_length. simpl.
+  rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r.
+  rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r.
+  rewrite <- Nat.add_0_l at 1. apply Nat.add_le_mono.
+  apply Nat.le_0_l. apply Nat.le_refl.
 
   (* inutile
   assert (V: nth_error (b4 :: b6 :: b9 :: tl) 2 = Some b9). reflexivity.
@@ -880,7 +885,7 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   destruct (Nat.testbit (m / 4) 0) ; [right | left] ; reflexivity.
   reflexivity.
   pose (lh := length ((b3 :: b5 :: b7 :: hd) ++ [b; b0; b1; b2])).
-  fold lh in H1.
+  fold lh in H1. fold lh in T.
 
   assert ({b9=b0} + {~ b9=b0}). apply bool_dec. destruct H8. rewrite e1 in H.
   (* si centre = 8n + 2, alors les cinq premiers sont absurdes *)
@@ -892,13 +897,26 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   assert (lh - 8 = 8 * Nat.pred (lh / 8) + 2).
   rewrite <- Nat.add_cancel_r with (p := 8). rewrite <- Nat.add_sub_swap.
   rewrite Nat.add_sub. rewrite Nat.add_shuffle0. rewrite <- Nat.mul_succ_r.
-  assumption.
+  assumption. assumption.
   
+  assert (nth_error (tm_step (3 + (n-3))) (Nat.pred (lh/8) * 8 + 3)
+        = nth_error (tm_step (3 + (n-3))) (Nat.pred (lh/8) * 8 + 4)).
+  rewrite Nat.add_comm. rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub.
+  rewrite H.
 
 
 
 
-Nat.div_mod: forall x y : nat, y <> 0 -> x = y * (x / y) + x mod y
+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).
+Proof.
+
+
 
 
   False, True, True, False, True, False, False, True, True, False, False