diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index d1ef92b..bb99ccb 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -902,9 +902,16 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   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.
+  rewrite H. rewrite Nat.mul_comm.
+  apply eq_S in H9. symmetry in H9. rewrite <- Nat.add_1_r in H9.
+  rewrite <- Nat.add_assoc in H9. rewrite Nat.add_1_r in H9.
+  rewrite H9.
+  apply eq_S in H9. rewrite <- Nat.add_1_r in H9.
+  rewrite <- Nat.add_assoc in H9. rewrite Nat.add_1_r in H9.
+  rewrite H9. unfold lh.
 
 
+  (* TODO: montrer l'absurdité avec le cas réel de tm_step_repeating_patterns *)
 
 
 Lemma tm_step_repeating_patterns :