diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 6f3b5bc..b3a8abd 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -868,10 +868,21 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   assert ({b8=b9} + {~ b8=b9}). apply bool_dec. destruct H7. rewrite e0 in H.
 
   (* premier sous-cas : b8 = b9, contradiction lié à repeating_patterns *)
-  assert ({b9=b0} + {~ b9=b0}). apply bool_dec. destruct H7. rewrite e1 in H.
-  (* si centre = 8n + 6, alors les cinq derniers sont absurdes *)
-  (* si centre = 8n + 2, alors les cinq premiers sont absurdes *)
+      (* lemme initial *)
+  assert (forall n : nat, n mod 4 = 2 -> n mod 8 = 2 \/ n mod 8 = 6).
+  intro m. intro A.
+  assert (m mod (4*2) = m mod 4 + 4 * ((m / 4) mod 2)).
+  apply Nat.mod_mul_r; easy. rewrite A in H7.
+  rewrite <- Nat.bit0_mod in H7. replace (4*2) with 8 in H7.
+  rewrite H7.
+  destruct (Nat.testbit (m / 4) 0) ; [right | left] ; reflexivity.
+  reflexivity.
 
+  assert ({b9=b0} + {~ b9=b0}). apply bool_dec. destruct H8. rewrite e1 in H.
+  (* si centre = 8n + 2, alors les cinq premiers sont absurdes *)
+  (* si centre = 8n + 6, alors les cinq derniers sont absurdes *)
+  apply H7 in H1. destruct H1.
+    (* on commence par supposer le centre en 8n+2 : hypothèse H1 *)
   
 
   False, True, True, False, True, False, False, True, True, False, False