diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 37726c6..a5c149b 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -1191,47 +1191,57 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   destruct s0. inversion H15. destruct s0. inversion H15.
   destruct s0. inversion H15. destruct s0; inversion H15.
   inversion H15. reflexivity.
-(*
-  assert (b13 = b0). destruct b13; destruct b1; destruct b0.
-  reflexivity. inversion H46. reflexivity. inversion H45.
-  inversion H45. reflexivity. inversion H45. reflexivity.
-  rewrite H17 in H15. rewrite H17 in H47. rewrite <- H47 in H15.
-  rewrite <- H47 in H33. rewrite <- H33 in H15.
-  rewrite <- H47 in H24. rewrite <- H24 in H15.
-  rewrite <- H47 in H26. rewrite <- H26 in H15.
-  rewrite <- H47 in H39. rewrite <- H39 in H15.
-  rewrite <- H47 in H41. rewrite <- H41 in H15.
-  rewrite <- H47 in H43. rewrite <- H43 in H15.
-  rewrite negb_involutive in H15. rewrite negb_involutive in H15.
-  fold s in H15.
- *)
   rewrite H17 in H.
 
+  (* à ce stade H est contradictoire *)
+  assert (even (length h0) = false).
+  replace (h0 ++ [b0; b0; b1; b1; b0; b0; b1; b1] ++ t0)
+    with (h0 ++ [b0] ++ [b0] ++ ([b1; b1; b0; b0; b1; b1] ++ t0)) in H.
+  assert (odd (length [b0]) = true). reflexivity. generalize H18.
+  generalize H. apply tm_step_odd_prefix_square. reflexivity.
+  replace (h0 ++ [b0; b0; b1; b1; b0; b0; b1; b1] ++ t0)
+    with (h0 ++ [b0;b0;b1;b1] ++ [b0;b0;b1;b1] ++ t0) in H.
+  assert (even (length h0) = true).
+  assert (even (length (h0 ++ [b0;b0;b1;b1])) = true).
+  assert (0 < length [b0;b0;b1;b1]). simpl. apply Nat.lt_0_succ.
+  generalize H19. generalize H. apply tm_step_square_pos.
+  rewrite app_length in H19. rewrite Nat.even_add in H19.
+  rewrite H18 in H19. inversion H19. rewrite H18 in H19.
+  inversion H19. reflexivity. reflexivity.
+  rewrite <- length_zero_iff_nil. rewrite Y''. easy.
 
-Lemma tm_morphism_app : forall (l1 l2 : list bool),
-  tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
-Lemma tm_morphism_app2 : forall (l hd tl : list bool),
-  tm_morphism l = hd ++ tl
-  -> even (length hd) = true
-  -> hd = tm_morphism (firstn (Nat.div2 (length hd)) l).
-Lemma tm_morphism_app3 : forall (l hd tl : list bool),
-  tm_morphism l = hd ++ tl
-  -> even (length hd) = true
-  -> tl = tm_morphism (skipn (Nat.div2 (length hd)) l).
-  
+  (* fin de la preuve, on a b8 <> b9 *)
+  right. rewrite U. simpl. injection. inversion H7. rewrite H9 in n6.
+  contradiction n6. reflexivity.
 
+  rewrite removelast_firstn_len. rewrite removelast_firstn_len. simpl.
+  rewrite <- length_zero_iff_nil. easy.
 
+  rewrite <- length_zero_iff_nil. 
+  rewrite removelast_firstn_len. easy.
 
+  apply Nat.lt_1_2. easy.
 
-  
+  (* désormais on a b <> b1 ; il suffit de montrer que b = b0 pour
+     arriver à un bloc de 2 contenant deux termes identiques *)
+  assert (b = b0). destruct b; destruct b1; destruct b0.
+  reflexivity. contradiction n2. reflexivity. reflexivity.
+  contradiction n1. reflexivity. contradiction n1. reflexivity.
+  reflexivity. contradiction n2. reflexivity. reflexivity.
+  rewrite H1 in H.
 
+  replace (
+    (b3 :: hd) ++ b0 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b0 :: b4 :: tl)
+    with (
+    (b3 :: hd) ++ [b0] ++ [b0]
+            ++ b1 :: b2 :: b2 :: b1 :: b0 :: b0 :: b4 :: tl) in H.
+  assert (even (length (b3 :: hd)) = false).
+  assert (odd (length [b0]) = true). reflexivity. generalize H2.
+  generalize H. apply tm_step_odd_prefix_square. rewrite H2 in Q.
+  inversion Q. reflexivity.
 
-Lemma tm_step_odd_prefix_square : forall (n : nat) (hd a tl : list bool),
-  tm_step n = hd ++ a ++ a ++ tl
-  -> odd (length a) = true -> even (length hd) = false.
-Theorem tm_step_square_pos : forall (n : nat) (hd a tl : list bool),
-  tm_step n = hd ++ a ++ a ++ tl
-  -> 0 < length a -> even (length (hd ++ a)) = true.
+  (* fin de la destructuration de a, désormais trop grand
+     cf. hypothèse I *)
 
 
 
@@ -1240,66 +1250,6 @@ Theorem tm_step_square_pos : forall (n : nat) (hd a tl : list bool),
 
 
 
-Proof.
-
-
-
-
-  False, True, True, False, True, False, False, True, True, False, False
-
-Admitted.
-
-
-                TFFT TFTF FTFT TFFT (µ de TF TT FF TF) pourquoi impossible ?
-                FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ?
-                  FTTFTFFT FTTFTF  (pb avec le repeating_pattern de 8 ???)
-                     TFT TFT FF TFT TFT (si on part sur 2 mod 8)
-                                        (idem en partant de la droite pour 6 mod 8)
-Le lemme repeating_patterns se base sur les huit premiers termes de TM :
-
-
-                  
-
-
-
-
-
-  (* si on a ensuite le bloc précédent identique aux deux premiers de a
-
-
-
-
-  (* TODO : terminer avec une inversion sur la longueur de a ;
-     le dernier but vient de la destructuration initiale de a *)
-
-
-
-      F T | T F    | T F ][ F T |    F T T F
-                   4n
-
- ou         F T    | T F ][ F T | T F
-                   4n ou 4n
-
-         F T   F T T F F T T F    T F  (centre 4n+2 ET 4n : contra)
-         T F   F T T F F T T F    T F  (centre : 4n+2)
-         F T   F T T F F T T F    F T  (centre : 4n)
-         T F   F T T F F T T F    F T  (cubes)  
-
-
-
-
-              -->   T F   F T    | T F ][ F T | T F  F T  (impossible : cubes)
-              -->   F T   F T    | T F ][ F T | T F  T F
-
-  Bilan : seulement deux cas possible de palindrome 8
-      F T | T F | T F ][ F T | F T | T F
-         4n+2         4n+2    (trivial)
-
-      F T | F T | T F ][ F T | T F | T F
-                      4n   (par examen des cinq premiers termes à gauche)
-
-   *)
-
 
 Lemma tm_step_palindromic_length_12 :
   forall (n : nat) (hd a tl : list bool),