diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index feb87b3..a17abc7 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -860,6 +860,7 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   rewrite e0 in H7. inversion H7. assumption.
   easy.
 
+  assert (V: nth_error (b4 :: b6 :: b9 :: tl) 2 = Some b9). reflexivity.
   
 
   False, True, True, False, True, False, False, True, True, False, False