diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 8818c84..b70d5d3 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -595,14 +595,52 @@ Proof.
                 (T F) | T F T F || F T F T | (T F)     diff + impossible à gauche
    *)
   assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1. rewrite e in H.
+(*
   assert (b2 = b0). destruct (b2); destruct b1; destruct b0.
   reflexivity. contradiction n0. reflexivity. reflexivity.
   contradiction n1. reflexivity. contradiction n1. reflexivity.
 reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
+ *)
 
-(* cas b = b1        T F T F || F T F T    *)
+  rewrite app_removelast_last with (l := b3::hd) (d := false) in H.
+  rewrite <- app_assoc in H.
+  assert ({last (b3::hd) false=b0} + {~ last (b3::hd) false=b0}).
+  apply bool_dec. destruct H1. rewrite e0 in H.
 
+  (* problème à gauche *)
+  destruct M. left. assumption. (* ici on postule le modulo = 2 *)
 
+  rewrite app_removelast_last with (l := b3::hd) (d := false) in Q.
+  rewrite last_length in Q. rewrite Nat.even_succ in Q. apply odd_mod4 in Q.
+  destruct Q.
+  assert (exists x, firstn 2 [b0;b1;b0;b1] = [x;x]). generalize H2.
+  assert (length [b0;b1;b0;b1] = 4). reflexivity. generalize H3.
+  replace (
+    removelast (b3 :: hd) ++
+    [b0] ++ b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl )
+    with (
+    removelast (b3 :: hd) ++ [b0;b1;b0;b1]
+      ++ (b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl )) in H.
+  generalize H. apply tm_step_factor4_1mod4. reflexivity.
+  destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
+  contradiction n1. reflexivity.
+
+  assert (exists x, skipn 2 [b0;b1;b0;b1] = [x;x]). generalize H2.
+  assert (length [b0;b1;b0;b1] = 4). reflexivity. generalize H3.
+  replace (
+    removelast (b3 :: hd) ++
+    [b0] ++ b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl )
+    with (
+    removelast (b3 :: hd) ++ [b0;b1;b0;b1]
+      ++ (b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl )) in H.
+  generalize H. apply tm_step_factor4_3mod4. reflexivity.
+  destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
+  contradiction n1. reflexivity. easy.
+
+(* nouveau cas : last (b3 :: hd) false <> b0
+                (F T) | T F T F || F T F T | (F T)     diff + impossible à droite
+                (F T) | T F T F || F T F T | (T F)     4n+2    a/rev a/a possible ?
+ *)