diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index c8ec5b2..d23cb05 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -1118,6 +1118,24 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   apply Nat.lt_succ_l in R. apply Nat.lt_succ_l in R. assumption.
   apply Nat.lt_1_2. reflexivity.
   (* now we have added b12 in front of tl *)
+    (* proof that b12 <> b1 *)
+  assert ({b12=b1} + {~ b12=b1}). apply bool_dec. destruct H10. rewrite e1 in H.
+  assert (even (length (hd'' ++ [b0;b1;b0;b1;b1; b0; b1; b0; b0; b1])) = false). 
+  replace ( hd'' ++ [b0] ++ [b1] ++ [b0] ++ [b1] ++ b1
+    :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: b0 :: b1 :: b1 :: tl)
+    with ((hd'' ++ [b0;b1;b0;b1;b1; b0; b1; b0; b0; b1])
+            ++ [ b0;b1;b1] ++ [b0;b1;b1] ++ tl) in H.
+  assert (odd (length [b0;b1;b1]) = true). reflexivity.
+  generalize H10. generalize H. apply tm_step_odd_prefix_square.
+  rewrite <- app_assoc. reflexivity. unfold hd'' in H10.
+  rewrite removelast_firstn_len in H10. rewrite Y'' in H10.
+  rewrite app_length in H10. rewrite firstn_length_le in H10. simpl in H10.
+  rewrite Nat.even_add in H10. 
+  simpl in Q. rewrite Q in H10. inversion H10.
+  rewrite Y''. apply Nat.le_pred_l.
+    (* now we know that b12 <> b1 *)
+
+