diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index d23cb05..22433e3 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -1134,7 +1134,12 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   simpl in Q. rewrite Q in H10. inversion H10.
   rewrite Y''. apply Nat.le_pred_l.
     (* now we know that b12 <> b1 *)
-
+  (* proof that b12 = b0 *)
+  assert (b12 = b0). destruct b12; destruct b1; destruct b0.
+  reflexivity. contradiction n8. reflexivity. reflexivity.
+  contradiction n1. reflexivity. contradiction n1. reflexivity.
+  reflexivity. contradiction n8. reflexivity. reflexivity.
+  rewrite H10 in H.