diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 78a9b83..e2c21d0 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -943,7 +943,13 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   rewrite <- Nat.add_le_mono_r. destruct hd. inversion Q.
   simpl. apply le_n_S. apply le_0_n. reflexivity. reflexivity.
   apply Nat.lt_le_incl. assumption.
+  rewrite <- tm_step_repeating_patterns in H10. inversion H10.
+  simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
+  simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
 
+  unfold lh.