diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 8644b04..75a0b03 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -1153,6 +1153,28 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   rewrite firstn_length_le. simpl in Q. rewrite Q. reflexivity.
   rewrite Y''. apply Nat.le_succ_diag_r. reflexivity.
 
+  (* destructuring n *)
+  destruct n. inversion H0. rewrite <- tm_step_lemma in H.
+
+  (* inverting tm_morphism in tm_step n *)
+  assert (hd'' = tm_morphism (firstn (Nat.div2 (length hd'')) (tm_step n))).
+  generalize H11. generalize H. apply tm_morphism_app2.
+
+  assert (s ++ tl = tm_morphism (skipn (Nat.div2 (length hd'')) (tm_step n))).
+  generalize H11. generalize H. apply tm_morphism_app3. symmetry in H13.
+
+  assert (even (length s) = true). unfold s. reflexivity.
+  assert (s = tm_morphism (firstn (Nat.div2 (length s))
+      (skipn (Nat.div2 (length hd'')) (tm_step n)))).
+  generalize H14. generalize H13. apply tm_morphism_app2.
+
+  assert (tl = tm_morphism (skipn (Nat.div2 (length s))
+      (skipn (Nat.div2 (length hd'')) (tm_step n)))).
+  generalize H14. generalize H13. apply tm_morphism_app3.
+
+  rewrite H12 in H. rewrite H15 in H. rewrite H16 in H.
+  rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
+  rewrite <- tm_morphism_eq in H.