diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 15c7980..23a4edd 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -803,6 +803,11 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   assumption. apply Nat.lt_1_2. reflexivity.
 
   (* termes à prouver *)
+  assert (Y: forall (k: bool) (x : list bool),
+    length (removelast (k::x)) = length x).
+  intros k x. rewrite removelast_firstn_len. simpl.
+  rewrite firstn_length_le. reflexivity. simpl.
+  apply Nat.le_succ_diag_r.
   assert (U: 
     nth_error (b3 :: b5 :: b7 :: hd) (length (b3 :: b5 :: b7 :: hd) - 3)
     = Some b8). unfold b8.
@@ -812,6 +817,14 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   rewrite app_removelast_last
     with (l := (removelast (removelast (b3::b5::b7::hd)))) (d := false) at 1.
   rewrite <- app_assoc. rewrite <- app_assoc. rewrite nth_error_app2.
+  rewrite removelast_firstn_len at 2. rewrite Y.
+  replace (length (b5::b7::hd)) with (S (S (length hd))).
+  rewrite <- pred_Sn. rewrite removelast_firstn. rewrite firstn_length_le.
+  replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))).
+  rewrite <- Nat.sub_add_distr. rewrite Nat.sub_diag.
+  reflexivity. reflexivity.
+  rewrite Y. simpl. 
+