diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index a5c149b..c5ff9bc 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -1242,7 +1242,10 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
 
   (* fin de la destructuration de a, désormais trop grand
      cf. hypothèse I *)
-
+  simpl in I. apply eq_add_S in I. apply eq_add_S in I.
+  apply eq_add_S in I. apply eq_add_S in I.
+  symmetry in I. apply O_S in I. contradiction I.
+Qed.