diff --git a/src/thue_morse.v b/src/thue_morse.v
index ea39049..fa7ae43 100644
--- a/src/thue_morse.v
+++ b/src/thue_morse.v
@@ -1287,6 +1287,7 @@ Lemma tm_step_factor4_1mod4 : forall (n' : nat) (w z y : list bool),
     tm_step n' = w ++ z ++ y
     -> length z = 4 -> length w mod 4 = 1
     -> exists (x : bool), firstn 2 z = [x;x].
+Proof.
   intros n' w z y. intros G0 G1 G2.
   assert (U: 4 * (length w / 4) <= length w).
   apply Nat.mul_div_le. easy.
diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 2333974..0346943 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -308,8 +308,14 @@ Lemma tm_step_palindromic_length_8 :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ (rev a) ++ tl
   -> length a = 4
-  -> length (hd ++ a) mod 4 = 0
-     \/ nth_error hd (length hd - 3) <> nth_error tl 2.
+  -> (
+       length (hd ++ a) mod 4 = 0
+       /\ exists b, a = [b; negb b; negb b; b]
+     ) \/ (
+       length (hd ++ a) mod 4 = 2
+       /\ (exists b, a = [b; negb b; b; negb b])
+       /\ nth_error hd (length hd - 3) <> nth_error tl 2
+     ).
 Proof.
   intros n hd a tl. intros H I.
 
@@ -450,30 +456,44 @@ Proof.
   rewrite <- app_assoc in H.
   assert ({last (b3::hd) false=b1} + {~ last (b3::hd) false=b1}).
   apply bool_dec. destruct H1. rewrite e0 in H.
+
+  assert (b2 = b). destruct b2; destruct b1; destruct b.
+  reflexivity. contradiction n0. reflexivity. reflexivity.
+  contradiction n1. reflexivity. contradiction n1. reflexivity.
+  reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
+
+  assert (R: b1 = negb b). destruct b; destruct b1;
+  reflexivity || ( rewrite H1 in n0; contradiction n0; reflexivity).
+
   (* un cas à étudier 
                 (??? T) | F T T F || F T T F | ???   impossible à gauche
   *)
-  destruct M. left. assumption. (* ici on postule le modulo = 2 *)
+  destruct M. left.
+  split. assumption.
+  rewrite e. rewrite R. rewrite H1. exists b. reflexivity.
 
+  (* suite *)
   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.
-  rewrite app_removelast_last with (l := b3::hd) (d := false) in H1.
+  rewrite app_removelast_last with (l := b3::hd) (d := false) in H2.
   destruct Q.
-  assert (exists x, firstn 2 [b1;b;b1;b1] = [x;x]). generalize H2.
-  assert (length [b1;b;b1;b1] = 4). reflexivity. generalize H3.
+  assert (exists x, firstn 2 [b1;b;b1;b1] = [x;x]). generalize H3.
+  assert (length [b1;b;b1;b1] = 4). reflexivity. generalize H4.
   replace (
     removelast (b3 :: hd) ++
-    [b1] ++ b :: b1 :: b1 :: b2 :: b2 :: b1 :: b1 :: b :: b4 :: tl )
+    [b1] ++ b :: b1 :: b1 :: b  :: b  :: b1 :: b1 :: b :: b4 :: tl )
     with (
     removelast (b3 :: hd) ++ [b1;b;b1;b1]
-      ++ (b2 :: b2 :: b1 :: b1 :: b :: b4 :: tl )) in H.
+      ++ (b :: b :: b1 :: b1 :: b :: b4 :: tl )) in H.
   generalize H. apply tm_step_factor4_1mod4. reflexivity.
-  destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
+  destruct H4. inversion H4. rewrite <- H7 in H6. rewrite H6 in n1.
   contradiction n1. reflexivity.
 
-  rewrite app_length in H1. rewrite app_length in H1.
-  rewrite <- Nat.add_assoc in H1. rewrite <- Nat.add_mod_idemp_l in H1.
-  rewrite H2 in H1. inversion H1. easy. easy. easy.
+  rewrite app_length in H2. rewrite app_length in H2.
+  rewrite <- Nat.add_assoc in H2. rewrite <- Nat.add_mod_idemp_l in H2.
+  rewrite H3 in H2. inversion H2.
+
+  easy. easy. easy.
 
   (* Deux cas
                 (T F) | F T T F || F T T F | (F T)  cube
@@ -483,23 +503,35 @@ Proof.
      (* un sous-cas :
                 (T F) | F T T F || F T T F | (T F)  impossible à droite
       *)
-  destruct M. left. assumption. (* ici on postule le modulo = 2 *)
 
-  rewrite e in H1.
+  assert (b2 = b). destruct b2; destruct b1; destruct b.
+  reflexivity. contradiction n0. reflexivity. reflexivity.
+  contradiction n1. reflexivity. contradiction n1. reflexivity.
+  reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
+
+  assert (R: b1 = negb b). destruct b; destruct b1;
+  reflexivity || ( rewrite H1 in n0; contradiction n0; reflexivity).
+
+  destruct M. left.
+  split. assumption. (* ici on postule le modulo = 2 *)
+  rewrite e. rewrite R. rewrite H1. exists b. reflexivity.
+
+  rewrite e in H2.
   assert (length (((b3 :: hd) ++ [b; b1; b1; b2]) ++ [b2]) mod 4 = 3).
-  rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite H1.
+  rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite H2.
   reflexivity. easy.
 
   replace(
     removelast (b3 :: hd) ++ [last (b3 :: hd) false] ++
-    b :: b1 :: b1 :: b2 :: b2 :: b1 :: b1 :: b :: b1 :: tl )
+    b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b1 :: tl )
   with (
-    (((b3 :: hd) ++ [b; b1; b1; b2]) ++ [b2]) ++ [b1; b1;b;b1] ++ tl) in H.
+    (((b3 :: hd) ++ [b; b1; b1; b]) ++ [b]) ++ [b1; b1;b;b1] ++ tl) in H.
 
-  assert (exists x, skipn 2 [b1;b1;b;b1] = [x;x]). generalize H2.
-  assert (length [b1;b1;b;b1] = 4). reflexivity. generalize H3.
+  rewrite H1 in H3.
+  assert (exists x, skipn 2 [b1;b1;b;b1] = [x;x]). generalize H3.
+  assert (length [b1;b1;b;b1] = 4). reflexivity. generalize H4.
   generalize H. apply tm_step_factor4_3mod4.
-  destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
+  destruct H4. inversion H4. rewrite <- H7 in H6. rewrite H6 in n1.
   contradiction n1. reflexivity.
   symmetry. rewrite app_assoc. rewrite <- app_removelast_last.
   rewrite <- app_assoc. rewrite <- app_assoc. reflexivity. easy.
@@ -601,8 +633,28 @@ reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
   apply bool_dec. destruct H1. rewrite e0 in H.
 
   (* problème à gauche *)
-  destruct M. left. assumption. (* ici on postule le modulo = 2 *)
+  destruct M.
 
+  (* problème avec n1 !!! *)
+  assert (T1: b0 = b1).
+  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.
+  assert (T2: exists (x : bool), firstn 2 [b1;b0;b1;b4] = [x;x]).
+  assert (length ((b3 :: hd) ++ [b; b0; b1; b2; b2]) mod 4 = 1).
+  replace ((b3 :: hd) ++ [b; b0; b1; b2; b2])
+    with (((b3 :: hd) ++ [b; b0; b1; b2]) ++ [b2]).
+  rewrite app_length. rewrite <- Nat.add_mod_idemp_l.
+  rewrite H1. reflexivity. easy. rewrite <- app_assoc. reflexivity.
+  generalize H2. assert (length ([b1;b0;b1;b4]) = 4). reflexivity.
+  generalize H3. generalize H. rewrite e. rewrite <- e0 at 1.
+  rewrite <- app_removelast_last. apply tm_step_factor4_1mod4.
+  easy. inversion T2. inversion H2. reflexivity.
+  rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
+  rewrite T1 in n1. contradiction n1. reflexivity.
+  
+  (* 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.
@@ -635,8 +687,27 @@ reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
                 (F T) | T F T F || F T F T | (T F)     4n+2    a/rev a/a possible ?
  *)
   (* régler d'abord la question du modulo au centre *)
-  destruct M. left. assumption. (* ici on postule le modulo = 2 *)
+  destruct M.
+  assert (T1: b0 = b1).
+  replace (removelast (b3 :: hd) ++ [last (b3::hd) false]
+      ++ b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl)
+    with (((removelast (b3 :: hd) ++ [last (b3::hd) false])
+      ++ [b1; b0; b1; b2; b2])
+      ++  [b1; b0; b1; b4] ++ tl) in H.
+  assert (T2: exists (x : bool), firstn 2 [b1;b0;b1;b4] = [x;x]).
+  assert (length ((b3 :: hd) ++ [b; b0; b1; b2; b2]) mod 4 = 1).
+  replace ((b3 :: hd) ++ [b; b0; b1; b2; b2])
+    with (((b3 :: hd) ++ [b; b0; b1; b2]) ++ [b2]).
+  rewrite app_length. rewrite <- Nat.add_mod_idemp_l.
+  rewrite H1. reflexivity. easy. rewrite <- app_assoc. reflexivity.
+  generalize H2. assert (length ([b1;b0;b1;b4]) = 4). reflexivity.
+  generalize H3. generalize H. rewrite e.
+  rewrite <- app_removelast_last. apply tm_step_factor4_1mod4.
+  easy. inversion T2. inversion H2. reflexivity.
+  rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
+  rewrite T1 in n1. contradiction n1. reflexivity.
 
+  (* on suppose maintenant le modulo = 2 *)
   assert (last (b3::hd) false = b1).
   destruct (last (b3::hd) false); destruct b1; destruct b0;
   reflexivity || contradiction n2 || contradiction n1; reflexivity.
@@ -851,10 +922,6 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   rewrite <- Nat.add_0_l at 1. apply Nat.add_le_mono.
   apply Nat.le_0_l. apply Nat.le_refl.
 
-  (* inutile
-  assert (V: nth_error (b4 :: b6 :: b9 :: tl) 2 = Some b9). reflexivity.
-   *)
-
   (* analyse finale *)
   assert ({b8=b9} + {~ b8=b9}). apply bool_dec. destruct H7. rewrite e0 in H.
 
@@ -938,7 +1005,7 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   rewrite Nat.add_lt_mono_r with (p := 8).
   rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub.
   rewrite <- Nat.add_assoc. replace (2+8) with 10.
-  replace (8) with (2^3) at 1. rewrite <- Nat.pow_add_r.
+  replace 8 with (2^3) at 1. rewrite <- Nat.pow_add_r.
   rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. simpl.
   rewrite <- tm_size_power2. rewrite H'. unfold lh.
   rewrite app_length. rewrite app_length. rewrite <- Nat.add_assoc.
@@ -1193,7 +1260,15 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
   rewrite <- length_zero_iff_nil. rewrite Y''. easy.
 
   (* fin de la preuve, on a b8 <> b9 *)
-  right. rewrite U. simpl. injection. inversion H7. rewrite H9 in n6.
+  right.
+  split. assumption.
+  split. rewrite H4. rewrite e.
+  assert (b0 = negb b1). destruct b0; destruct b1.
+  contradiction n1. reflexivity. reflexivity. reflexivity.
+  contradiction n1. reflexivity. rewrite H7. exists b1.
+  reflexivity.
+
+  rewrite U. simpl. injection. inversion H7. rewrite H9 in n6.
   contradiction n6. reflexivity.
 
   rewrite removelast_firstn_len. rewrite removelast_firstn_len. simpl.
@@ -1262,11 +1337,17 @@ Proof.
   rewrite <- app_assoc in H.
   pose (tl' := rev (firstn (length a - 4) a) ++ tl). fold tl' in H.
 
-  assert (K: length (hd' ++ a') mod 4 = 0
-    \/ nth_error hd' (length hd' - 3) <> nth_error tl' 2).
+  assert (K: (
+       length (hd' ++ a') mod 4 = 0
+       /\ exists b, a' = [b; negb b; negb b; b]
+     ) \/ (
+       length (hd' ++ a') mod 4 = 2
+       /\ (exists b, a' = [b; negb b; b; negb b])
+       /\ nth_error hd' (length hd' - 3) <> nth_error tl' 2
+     )).
   fold a' in H1. generalize H1. generalize H.
   apply tm_step_palindromic_length_8.
-  destruct K.
+  destruct K. destruct H2.
   unfold hd' in H2. unfold a' in H2. rewrite <- app_assoc in H2.
   rewrite firstn_skipn in H2. assumption.
 
@@ -1280,6 +1361,7 @@ Proof.
   apply Nat.succ_lt_mono in I. apply Nat.succ_lt_mono in I. 
   inversion I.
 
+  destruct H2 as [H2' H2'']. destruct H2'' as [H2'' H2].
   unfold hd' in H2. unfold tl' in H2.
   rewrite nth_error_app2 in H2. rewrite nth_error_app1 in H2.
   rewrite app_length in H2. rewrite Nat.add_comm in H2.
diff --git a/src/thue_morse4.v b/src/thue_morse4.v
index 927bb78..02ad65c 100644
--- a/src/thue_morse4.v
+++ b/src/thue_morse4.v
@@ -827,3 +827,1011 @@ Proof.
     destruct H2.
     + assert (E := H2). apply Nat.Even_double in H2. rewrite <- H2 in H1.
 Abort.
+
+
+
+
+
+
+(* palidrome 2*4 : soit centré en 4n soit pas plus de 2*6 *)
+(* modifier l'énoncé : ajouter le modulo = 2 ET la différence sur le 7ème
+      ET existence d'un palindrome 2 * - *)
+Lemma tm_step_palindromic_length_8_bis :
+  forall (n : nat) (hd a tl : list bool),
+  tm_step n = hd ++ a ++ (rev a) ++ tl
+  -> length a = 4
+  -> (
+       length (hd ++ a) mod 4 = 0
+       /\ exists b, a = [b; negb b; negb b; b]
+     ) \/ (
+       length (hd ++ a) mod 4 = 2
+       /\ (exists b, a = [b; negb b; b; negb b])
+       /\ nth_error hd (length hd - 3) <> nth_error tl 2
+     ).
+Proof.
+  intros n hd a tl. intros H I.
+
+  (* proof that length hd++a is even *)
+  assert (P: even (length (hd ++ a)) = true).
+  assert (0 < length a). rewrite I. apply Nat.lt_0_succ. generalize H0.
+  generalize H. apply tm_step_palindromic_even_center.
+
+  assert (M: length (hd ++ a) mod 4 = 0 \/ length (hd ++ a) mod 4 = 2).
+  generalize P. apply even_mod4.
+
+  (* proof that length hd is even *)
+  assert (Q: even (length hd) = true). rewrite app_length in P.
+  rewrite Nat.even_add_even in P. assumption. rewrite I.
+  apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
+
+  (* construction de a *)
+  destruct a. inversion I. destruct a. inversion I.
+  destruct a. inversion I. destruct a. inversion I.
+  destruct a. simpl in H.
+
+  (* proof that b1 <> b2 *)
+  assert ({b1=b2} + {~ b1=b2}). apply bool_dec. destruct H0.
+  replace (hd ++ b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl)
+    with ((hd ++ b :: b0 :: nil)
+              ++ [b1] ++ [b2] ++ [b2] ++  b1 :: b0 :: b :: tl) in H.
+  rewrite e in H. apply tm_step_cubefree in H. contradiction H.
+  reflexivity. apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
+
+  (* proof that n > 2 *)
+  assert (2 < n).
+  assert (J: 0 + length (b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl)
+        <= length hd
+            + length (b :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b :: tl)).
+  apply Nat.add_le_mono. apply Nat.le_0_l. apply Nat.le_refl.
+  rewrite Nat.add_0_l in J. rewrite <- app_length in J. rewrite <- H in J.
+  rewrite tm_size_power2 in J.
+  destruct n. inversion J. apply Nat.nle_succ_0 in H1. contradiction H1.
+  destruct n. inversion J. inversion H1.
+  apply Nat.nle_succ_0 in H3. contradiction H3.
+  destruct n. inversion J. inversion H1. inversion H3. inversion H5.
+  inversion H7. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  apply Nat.lt_0_succ.
+
+  (* proof that hd <> nil *)
+  destruct hd.
+  assert (Z: 4 < 2^n). replace 4 with (2^2).
+  apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.
+  assert (Some b2 = nth_error (tm_step n) 3). rewrite H. reflexivity.
+  replace (nth_error (tm_step n) 3) with (nth_error (tm_step 3) 3) in H1.
+  simpl in H1.
+  assert (Some b2 = nth_error (tm_step n) 4). rewrite H. reflexivity.
+  replace (nth_error (tm_step n) 4) with (nth_error (tm_step 3) 4) in H2.
+  simpl in H2.
+  rewrite H1 in H2. inversion H2. apply tm_step_stable. simpl.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  apply Nat.lt_0_succ. assumption. apply tm_step_stable. simpl.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
+  assert (3 < 4).
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
+  generalize Z. generalize H2. apply Nat.lt_trans.
+  
+  (* proof that tl <> nil *)
+  destruct tl.
+
+  assert (Z: 4 < 2^n). replace 4 with (2^2).
+  apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. assumption.
+
+  assert (Y: tm_step n = rev (tm_step n)
+        \/ tm_step n = map negb (rev (tm_step n))). apply tm_step_rev.
+  destruct Y; rewrite H in H1 at 2; rewrite rev_app_distr in H1.
+
+  assert (Some b2 = nth_error (tm_step n) 3). rewrite H1. reflexivity.
+  replace (nth_error (tm_step n) 3) with (nth_error (tm_step 3) 3) in H2.
+  simpl in H2.
+  assert (Some b2 = nth_error (tm_step n) 4). rewrite H1. reflexivity.
+  replace (nth_error (tm_step n) 4) with (nth_error (tm_step 3) 4) in H3.
+  simpl in H3.
+  rewrite H2 in H3. inversion H3. apply tm_step_stable. simpl.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  apply Nat.lt_0_succ. assumption. apply tm_step_stable. simpl.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
+  assert (3 < 4).
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
+  generalize Z. generalize H3. apply Nat.lt_trans.
+
+  assert (Some (negb b2) = nth_error (tm_step n) 3). rewrite H1.
+  rewrite nth_error_map. reflexivity.
+  replace (nth_error (tm_step n) 3) with (nth_error (tm_step 3) 3) in H2.
+  simpl in H2.
+  assert (Some (negb b2) = nth_error (tm_step n) 4). rewrite H1.
+  rewrite nth_error_map. reflexivity.
+  replace (nth_error (tm_step n) 4) with (nth_error (tm_step 3) 4) in H3.
+  simpl in H3.
+  rewrite H2 in H3. inversion H3. apply tm_step_stable. simpl.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  apply Nat.lt_0_succ. assumption. apply tm_step_stable. simpl.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
+  assert (3 < 4).
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
+  generalize Z. generalize H3. apply Nat.lt_trans.
+
+  (* FIRST PART OF THE PROOF: case b0 = b1 *)
+  (* première hypothèse   b0 = b1 mais alors on construit vers la
+     gauche jusqu'à  (lest hd) et l'on a dans l'ordre jusqu'au centre :
+       b1 | (negb b1) b1 | b1 (negb b1  ||
+     et les quatre premiers termes vont impliquer que le centre soit en 4n+2 *)
+  assert ({b0=b1} + {~ b0=b1}). apply bool_dec. destruct H1.
+  rewrite e in H.
+
+  (* on a alors b = negb b1 (car dans le même bloc pair on a 01 ou 10 *)
+  assert ({b=b1} + {~ b=b1}). apply bool_dec. destruct H1.
+  rewrite e0 in H.
+  replace
+    ((b3 :: hd) ++ b1 :: b1 :: b1 :: b2 :: b2 :: b1 :: b1 :: b1 :: b4 :: tl)
+    with
+      ((b3 :: hd) ++ [b1] ++ [b1] ++ [b1]
+              ++ b2 :: b2 :: b1 :: b1 :: b1 :: b4 :: tl) in H.
+  apply tm_step_cubefree in H. contradiction H. reflexivity.
+  apply Nat.lt_0_1. reflexivity.
+
+  (* à ce stade on a F T | T F || F T T F
+        trois cas :
+              (??? T) | F T T F || F T T F | ???   impossible à gauche
+                (T F) | F T T F || F T T F | (F T)  cube
+                (T F) | F T T F || F T T F | (T F)   OK, diff + impossible à droite
+   *)
+  rewrite app_removelast_last with (l := b3::hd) (d := false) in H.
+  rewrite <- app_assoc in H.
+  assert ({last (b3::hd) false=b1} + {~ last (b3::hd) false=b1}).
+  apply bool_dec. destruct H1. rewrite e0 in H.
+
+  assert (b2 = b). destruct b2; destruct b1; destruct b.
+  reflexivity. contradiction n0. reflexivity. reflexivity.
+  contradiction n1. reflexivity. contradiction n1. reflexivity.
+  reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
+
+  assert (R: b1 = negb b). destruct b; destruct b1;
+  reflexivity || ( rewrite H1 in n0; contradiction n0; reflexivity).
+
+  (* un cas à étudier 
+                (??? T) | F T T F || F T T F | ???   impossible à gauche
+  *)
+  destruct M. left.
+  split. assumption.
+  rewrite e. rewrite R. rewrite H1. exists b. reflexivity.
+
+  (* suite *)
+  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.
+  rewrite app_removelast_last with (l := b3::hd) (d := false) in H2.
+  destruct Q.
+  assert (exists x, firstn 2 [b1;b;b1;b1] = [x;x]). generalize H3.
+  assert (length [b1;b;b1;b1] = 4). reflexivity. generalize H4.
+  replace (
+    removelast (b3 :: hd) ++
+    [b1] ++ b :: b1 :: b1 :: b  :: b  :: b1 :: b1 :: b :: b4 :: tl )
+    with (
+    removelast (b3 :: hd) ++ [b1;b;b1;b1]
+      ++ (b :: b :: b1 :: b1 :: b :: b4 :: tl )) in H.
+  generalize H. apply tm_step_factor4_1mod4. reflexivity.
+  destruct H4. inversion H4. rewrite <- H7 in H6. rewrite H6 in n1.
+  contradiction n1. reflexivity.
+
+  rewrite app_length in H2. rewrite app_length in H2.
+  rewrite <- Nat.add_assoc in H2. rewrite <- Nat.add_mod_idemp_l in H2.
+  rewrite H3 in H2. inversion H2.
+
+  easy. easy. easy.
+
+  (* Deux cas
+                (T F) | F T T F || F T T F | (F T)  cube
+                (T F) | F T T F || F T T F | (T F)  impossible à droite
+  *)
+  assert ({b4=b1} + {~ b4=b1}). apply bool_dec. destruct H1. rewrite e0 in H.
+     (* un sous-cas :
+                (T F) | F T T F || F T T F | (T F)  impossible à droite
+      *)
+
+  assert (b2 = b). destruct b2; destruct b1; destruct b.
+  reflexivity. contradiction n0. reflexivity. reflexivity.
+  contradiction n1. reflexivity. contradiction n1. reflexivity.
+  reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H1 in H.
+
+  assert (R: b1 = negb b). destruct b; destruct b1;
+  reflexivity || ( rewrite H1 in n0; contradiction n0; reflexivity).
+
+  destruct M. left.
+  split. assumption. (* ici on postule le modulo = 2 *)
+  rewrite e. rewrite R. rewrite H1. exists b. reflexivity.
+
+  rewrite e in H2.
+  assert (length (((b3 :: hd) ++ [b; b1; b1; b2]) ++ [b2]) mod 4 = 3).
+  rewrite app_length. rewrite <- Nat.add_mod_idemp_l. rewrite H2.
+  reflexivity. easy.
+
+  replace(
+    removelast (b3 :: hd) ++ [last (b3 :: hd) false] ++
+    b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b1 :: tl )
+  with (
+    (((b3 :: hd) ++ [b; b1; b1; b]) ++ [b]) ++ [b1; b1;b;b1] ++ tl) in H.
+
+  rewrite H1 in H3.
+  assert (exists x, skipn 2 [b1;b1;b;b1] = [x;x]). generalize H3.
+  assert (length [b1;b1;b;b1] = 4). reflexivity. generalize H4.
+  generalize H. apply tm_step_factor4_3mod4.
+  destruct H4. inversion H4. rewrite <- H7 in H6. rewrite H6 in n1.
+  contradiction n1. reflexivity.
+  symmetry. rewrite app_assoc. rewrite <- app_removelast_last.
+  rewrite <- app_assoc. rewrite <- app_assoc. reflexivity. easy.
+
+  (* un sous-cas
+                (T F) | F T T F || F T T F | (F T)  cube
+  *)
+  assert (b4 = b). destruct b4; destruct b1; destruct b;
+  reflexivity || contradiction n3 || contradiction n1; reflexivity.
+  rewrite H1 in H.
+  assert (b2 = b). destruct b2; destruct b1; destruct b.
+  reflexivity. contradiction n0. reflexivity. reflexivity.
+  contradiction n1. reflexivity. contradiction n1. reflexivity.
+  reflexivity. contradiction n0. reflexivity. reflexivity. rewrite H2 in H.
+  assert (last (b3::hd) false = b).
+  destruct (last (b3::hd) false); destruct b1; destruct b;
+  reflexivity || contradiction n2 || contradiction n1; reflexivity.
+
+       (* élargir hd et tl à l'aide des booléens b5 (gauche) et b6 (droite) *)
+  destruct hd. inversion Q. destruct tl.
+  assert (0 < n). apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption.
+  apply tm_step_length_even in H4. rewrite H in H4.
+  rewrite app_assoc in H4. rewrite <- app_removelast_last in H4.
+  rewrite app_length in H4. rewrite Nat.even_add in H4.
+  rewrite Q in H4. inversion H4. easy. rewrite H3 in H.
+  rewrite app_removelast_last
+         with (l := removelast (b3::b5::hd)) (d := false) in H.
+  rewrite <- app_assoc in H.
+
+  (* assigner
+       last (removelast (b3 :: b5 :: hd)) false = b1
+       b6 = b1
+   *)
+  assert ({last (removelast (b3 :: b5 :: hd)) false=b}
+            + {~ last (removelast (b3 :: b5 :: hd)) false=b}). apply bool_dec.
+  destruct H4. rewrite e0 in H.
+  replace (
+    removelast (removelast (b3 :: b5 :: hd)) ++ [b] ++ [b]
+      ++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b6 :: tl)
+    with (
+    removelast (removelast (b3 :: b5 :: hd)) ++ [b] ++ [b] ++ [b]
+      ++ b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b6 :: tl) in H.
+  apply tm_step_cubefree in H. contradiction H. reflexivity.
+  apply Nat.lt_0_1. reflexivity.
+  assert (last (removelast (b3 :: b5 :: hd)) false = b1).
+  destruct (last (removelast (b3 :: b5 :: hd)) false); destruct b1; destruct b.
+  reflexivity. reflexivity. contradiction n4. reflexivity.
+  contradiction n1. reflexivity. contradiction n1. reflexivity.
+  contradiction n4. reflexivity. reflexivity. reflexivity. rewrite H4 in H.
+  assert ({b6=b} + {~ b6=b}). apply bool_dec. destruct H5. rewrite e0 in H.
+  replace (
+    removelast (removelast (b3 :: b5 :: hd)) ++ [b1] ++ [b]
+      ++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b :: tl)
+    with (
+    (removelast (removelast (b3 :: b5 :: hd)) ++ [b1] ++ [b]
+      ++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: nil)
+      ++ [b] ++ [b] ++ [b] ++ tl) in H.
+  apply tm_step_cubefree in H. contradiction H. reflexivity.
+  apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.
+  assert (b6 = b1). destruct (b6); destruct b1; destruct b;
+  reflexivity || contradiction n5 || contradiction n1; reflexivity.
+  rewrite H5 in H.
+
+  (* contradiction *)
+  replace (
+    removelast (removelast (b3 :: b5 :: hd)) ++
+    [b1] ++ [b] ++ b :: b1 :: b1 :: b :: b :: b1 :: b1 :: b :: b :: b1 :: tl)
+    with (removelast (removelast (b3 :: b5 :: hd)) ++
+    [b1;b;b;b1] ++ [b1;b;b;b1] ++ [b1;b;b;b1] ++ tl) in H.
+  apply tm_step_cubefree in H. contradiction H. reflexivity.
+  apply Nat.lt_0_succ. reflexivity. easy. easy.
+
+  assert (H' := H).
+
+  (* SECOND PART PF THE PROOF: case b0 <> b1 *)
+  (* sinon, sur la base de    T F T F || F T F T
+        quatre cas :
+                (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 ?
+     empiriquement : n'apparaît jamais
+                   remonter encore d'un cran et prouver la différence à ce stade,
+                TFFT TFTF FTFT TFFT (µ de TF TT FF TF) pourquoi impossible ?
+                FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ?
+                     revoir l'énoncé en fonction
+                (T F) | T F T F || F T F T | (F T)     cube
+                (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.
+ *)
+
+  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.
+
+  (* problème avec n1 !!! *)
+  assert (T1: b0 = b1).
+  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.
+  assert (T2: exists (x : bool), firstn 2 [b1;b0;b1;b4] = [x;x]).
+  assert (length ((b3 :: hd) ++ [b; b0; b1; b2; b2]) mod 4 = 1).
+  replace ((b3 :: hd) ++ [b; b0; b1; b2; b2])
+    with (((b3 :: hd) ++ [b; b0; b1; b2]) ++ [b2]).
+  rewrite app_length. rewrite <- Nat.add_mod_idemp_l.
+  rewrite H1. reflexivity. easy. rewrite <- app_assoc. reflexivity.
+  generalize H2. assert (length ([b1;b0;b1;b4]) = 4). reflexivity.
+  generalize H3. generalize H. rewrite e. rewrite <- e0 at 1.
+  rewrite <- app_removelast_last. apply tm_step_factor4_1mod4.
+  easy. inversion T2. inversion H2. reflexivity.
+  rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
+  rewrite T1 in n1. contradiction n1. reflexivity.
+  
+  (* 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 ?
+ *)
+  (* régler d'abord la question du modulo au centre *)
+  destruct M.
+  assert (T1: b0 = b1).
+  replace (removelast (b3 :: hd) ++ [last (b3::hd) false]
+      ++ b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b4 :: tl)
+    with (((removelast (b3 :: hd) ++ [last (b3::hd) false])
+      ++ [b1; b0; b1; b2; b2])
+      ++  [b1; b0; b1; b4] ++ tl) in H.
+  assert (T2: exists (x : bool), firstn 2 [b1;b0;b1;b4] = [x;x]).
+  assert (length ((b3 :: hd) ++ [b; b0; b1; b2; b2]) mod 4 = 1).
+  replace ((b3 :: hd) ++ [b; b0; b1; b2; b2])
+    with (((b3 :: hd) ++ [b; b0; b1; b2]) ++ [b2]).
+  rewrite app_length. rewrite <- Nat.add_mod_idemp_l.
+  rewrite H1. reflexivity. easy. rewrite <- app_assoc. reflexivity.
+  generalize H2. assert (length ([b1;b0;b1;b4]) = 4). reflexivity.
+  generalize H3. generalize H. rewrite e.
+  rewrite <- app_removelast_last. apply tm_step_factor4_1mod4.
+  easy. inversion T2. inversion H2. reflexivity.
+  rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
+  rewrite T1 in n1. contradiction n1. reflexivity.
+
+  (* on suppose maintenant le modulo = 2 *)
+  assert (last (b3::hd) false = b1).
+  destruct (last (b3::hd) false); destruct b1; destruct b0;
+  reflexivity || contradiction n2 || contradiction n1; reflexivity.
+
+  assert ({b4=b0} + {~ b4=b0}). apply bool_dec. destruct H3. rewrite e0 in H.
+  assert (exists x, skipn 2 [b1;b0;b1;b0] = [x;x]).
+  replace (removelast (b3 :: hd) ++ [last (b3 :: hd) false] ++
+    b1 :: b0 :: b1 :: b2 :: b2 :: b1 :: b0 :: b1 :: b0 :: tl)
+    with (((b3 :: hd) ++ [b1;b0;b1;b2;b2])
+      ++ [b1;b0;b1;b0] ++ tl) in H.
+  assert (length ((b3::hd) ++ [b1; b0; b1; b2; b2]) mod 4 = 3). rewrite e in H1.
+  replace ([b1;b0;b1;b2;b2]) with ([b1;b0;b1;b2] ++ [b2]).
+  rewrite app_assoc. rewrite app_length. rewrite <- Nat.add_mod_idemp_l.
+  rewrite H1. reflexivity. easy. reflexivity.
+  assert (length [b1;b0;b1;b0] = 4). reflexivity.
+  generalize H3. generalize H4. generalize H. apply tm_step_factor4_3mod4.
+  symmetry. rewrite app_assoc. rewrite <- app_removelast_last.
+  rewrite <- app_assoc. reflexivity. easy.
+  destruct H3. inversion H3. rewrite <- H6 in H5. rewrite H5 in n1.
+  contradiction n1. reflexivity.
+
+  assert (b4 = b1). destruct b4; destruct b1; destruct b0;
+  reflexivity || contradiction n3 || contradiction n1; reflexivity.
+  rewrite H3 in H. rewrite H2 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 H4 in H.
+
+  (* dernier cas (difficile
+                (F T) | T F T F || F T F T | (T F)     4n+2    a/rev a/a possible ?
+                remarquer le schéma    a ++ (rev a) ++ a
+     apparaît jusqu'à six termes à gauche et à droite
+     empiriquement : n'apparaît jamais avec un 7ème palindromique ajouté
+                   remonter encore d'un cran et prouver la différence à ce stade,
+                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 :
+[False, True, True, False, True, False, False, True]
+  --> il y a une contradiction à chaque fois
+  *)
+
+  (* on prouve 3 < n *)
+  assert (R: 2^3 < length (tm_step n)). rewrite H.
+  rewrite app_length. rewrite <- Nat.add_0_l at 1.
+  apply Nat.add_le_lt_mono. apply Nat.le_0_l. simpl.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  apply Nat.lt_0_succ. rewrite tm_size_power2 in R.
+  rewrite <- Nat.pow_lt_mono_r_iff in R.
+
+  (* on étend hd *)
+  destruct hd. inversion Q.
+  rewrite app_removelast_last
+      with (l := removelast (b3::b5::hd)) (d := false) in H.
+  assert ({last (removelast (b3 :: b5 :: hd)) false = b1}
+            + {~ last (removelast (b3 :: b5 :: hd)) false = b1}).
+  apply bool_dec. destruct H5. rewrite e0 in H.
+  rewrite <- app_assoc in H.
+  replace (b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: tl)
+    with ([b1] ++ b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: tl) in H.
+  apply tm_step_cubefree in H. contradiction H. reflexivity.
+  apply Nat.lt_0_1. reflexivity.
+
+  (* on étend tl*)
+  destruct tl.
+  assert (tm_step n = rev (tm_step n)
+           \/ tm_step n = map negb (rev (tm_step n))).
+  apply tm_step_rev. destruct H5; rewrite H in H5 at 2;
+  rewrite rev_app_distr in H5; simpl in H5;
+  assert (odd 0 = true).
+  assert (nth_error (tm_step n) (S (2*0) * 2^0) =
+          nth_error (tm_step n) (pred (S (2*0) * 2^0))).
+  rewrite H5. reflexivity. generalize H6.
+  apply tm_step_pred. simpl. rewrite <- Nat.pow_0_r with (a := 2) at 1.
+  apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
+  apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption. inversion H6.
+  assert (nth_error (tm_step n) (S (2*0) * 2^0) =
+          nth_error (tm_step n) (pred (S (2*0) * 2^0))).
+  rewrite H5. reflexivity. generalize H6.
+  apply tm_step_pred. simpl. rewrite <- Nat.pow_0_r with (a := 2) at 1.
+  apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
+  apply Nat.lt_succ_l. apply Nat.lt_succ_l. assumption. inversion H6.
+  assert ({b6=b1} + {~ b6=b1}). apply bool_dec. destruct H5. rewrite e0 in H.
+  replace (
+    (removelast (removelast (b3 :: b5 :: hd)) ++
+     [last (removelast (b3 :: b5 :: hd)) false]) ++
+    [b1] ++ b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: b1 :: tl)
+    with (
+    (removelast (removelast (b3 :: b5 :: hd)) ++
+     [last (removelast (b3 :: b5 :: hd)) false] ++
+    [b1] ++ b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: nil)
+      ++ [b1] ++ [b1] ++ [b1] ++ tl) in H.
+  apply tm_step_cubefree in H. contradiction H. reflexivity.
+  apply Nat.lt_0_1.
+  rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
+  rewrite <- app_assoc. reflexivity.
+
+  (* on assigne les valeurs correctes aux deux extrémités *)
+  assert (b6 = b0). destruct b6; destruct b1; destruct b0;
+  reflexivity || contradiction n5 || contradiction n1; reflexivity.
+  rewrite H5 in H.
+  assert (last (removelast (b3 :: b5 :: hd)) false = b0).
+  destruct (last (removelast (b3 :: b5 :: hd)) false);
+  destruct b1; destruct b0;
+  reflexivity || contradiction n4 || contradiction n1; reflexivity.
+  rewrite H6 in H.
+
+  (* on étend hd *)
+  destruct hd. simpl in H. assert (odd 3 = true). reflexivity.
+  rewrite <- tm_step_pred with (n := n) (k := 0) in H7.
+  rewrite H in H7. simpl in H7. inversion H7. rewrite H9 in n1.
+  contradiction n1. reflexivity. simpl.
+  replace 8 with (2^3). rewrite <- Nat.pow_lt_mono_r_iff.
+  assumption. apply Nat.lt_1_2. reflexivity.
+  rewrite app_removelast_last
+      with (l := removelast (removelast (b3::b5::b7::hd))) (d := false) in H.
+  pose (b8 := last (removelast (removelast (b3 :: b5 :: b7 :: hd))) false).
+  fold b8 in H. rewrite <- app_assoc in H. rewrite <- app_assoc in H.
+  pose (hd' := removelast (removelast (removelast (b3 :: b5 :: b7 :: hd)))).
+  fold hd' in H.
+
+  (* on étend tl *)
+  destruct tl.
+  assert (tm_step n = rev (tm_step n)
+           \/ tm_step n = map negb (rev (tm_step n))).
+  apply tm_step_rev. destruct H7; rewrite H in H7 at 2;
+  rewrite rev_app_distr in H7; simpl in H5.
+  assert (odd 3 = true). reflexivity.
+  rewrite <- tm_step_pred with (n := n) (k := 0) in H8.
+  rewrite H7 in H8. simpl in H8. inversion H8. rewrite H10 in n1.
+  contradiction n1. reflexivity. simpl.
+  replace 8 with (2^3). rewrite <- Nat.pow_lt_mono_r_iff.
+  assumption. apply Nat.lt_1_2. reflexivity.
+  assert (odd 3 = true). reflexivity.
+  rewrite <- tm_step_pred with (n := n) (k := 0) in H8.
+  rewrite H7 in H8. simpl in H8. inversion H8.
+  destruct b0; destruct b1. contradiction n1. reflexivity.
+  inversion H10. inversion H10. contradiction n1. reflexivity. simpl.
+  replace 8 with (2^3). rewrite <- Nat.pow_lt_mono_r_iff.
+  assumption. apply Nat.lt_1_2. reflexivity.
+
+  (* termes à prouver *)
+        (* lemmes initiaux *)
+  assert (Y: forall (k : bool) (x : list bool),
+    length (removelast (k::x)) = length x).
+  intros k x. rewrite removelast_firstn_len.
+  replace (length (k::x)) with (S (length x)). rewrite Nat.pred_succ.
+  rewrite firstn_length. simpl. apply Nat.min_l. apply Nat.le_succ_diag_r.
+  reflexivity.
+  assert (Y': forall (k1 k2 : bool) (x : list bool),
+    length (removelast (removelast (k1::k2::x))) = length x).
+  intros k1 k2 x.
+  rewrite removelast_firstn_len. rewrite Y.
+  replace (length (k2::x)) with (S (length x)).
+  rewrite Nat.pred_succ. rewrite firstn_length. rewrite Y.
+  apply Nat.min_l. apply Nat.le_succ_diag_r. reflexivity.
+  assert (Y'': forall (k1 k2 k3 : bool) (x : list bool),
+    length (removelast (removelast (removelast (k1::k2::k3::x)))) = length x).
+  intros k1 k2 k3 x.
+  rewrite removelast_firstn_len. rewrite removelast_firstn_len.
+  rewrite Y. replace (length (k2::k3::x)) with (S (length (k3::x))).
+  rewrite Nat.pred_succ. rewrite firstn_length.
+  rewrite firstn_length. rewrite Y. rewrite Nat.min_l. rewrite Nat.min_l.
+  reflexivity. apply Nat.le_succ_diag_r. rewrite Nat.min_l.
+  replace (length (k3 :: x)) with (S (length x)). rewrite Nat.pred_succ.
+  apply Nat.le_succ_diag_r. reflexivity.
+  replace (length (k2 :: k3::x)) with (S (length (k3::x))).
+  apply Nat.le_succ_diag_r. reflexivity. reflexivity.
+
+    (* preuves *)
+  assert (U: 
+    nth_error (b3 :: b5 :: b7 :: hd) (length (b3 :: b5 :: b7 :: hd) - 3)
+    = Some b8). unfold b8.
+  rewrite app_removelast_last with (l := b3::b5::b7::hd) (d := false) at 1.
+  rewrite app_removelast_last
+    with (l := (removelast (b3::b5::b7::hd))) (d := false) at 1.
+  rewrite app_removelast_last
+    with (l := (removelast (removelast (b3::b5::b7::hd)))) (d := false) at 1.
+  rewrite <- app_assoc. rewrite <- app_assoc. rewrite nth_error_app2.
+  rewrite Y''. rewrite <- Nat.sub_add_distr.
+  replace (length (b3::b5::b7::hd)) with (3 + length hd).
+  rewrite Nat.sub_diag. reflexivity. reflexivity. rewrite Y''.
+  replace (length (b3::b5::b7::hd)) with (length hd + 3).
+  rewrite Nat.add_sub. apply Nat.le_refl. rewrite Nat.add_comm.
+  reflexivity.
+  assert (0 < length (removelast (removelast (b3 :: b5 :: b7 :: hd)))).
+  rewrite Y'. simpl. apply Nat.lt_0_succ.
+  assert ({removelast (removelast (b3 :: b5 :: b7 :: hd))=nil}
+            + {~ removelast (removelast (b3 :: b5 :: b7 :: hd))=nil}).
+  apply list_eq_dec. apply bool_dec. destruct H8.
+  rewrite e0 in H7. inversion H7. assumption.
+  assert (0 < length (removelast (b3 :: b5 :: b7 :: hd))).
+  rewrite Y. simpl. apply Nat.lt_0_succ.
+  assert ({removelast (b3 :: b5 :: b7 :: hd)=nil}
+            + {~ removelast (b3 :: b5 :: b7 :: hd)=nil}).
+  apply list_eq_dec. apply bool_dec. destruct H8.
+  rewrite e0 in H7. inversion H7. assumption.
+  easy.
+
+  assert (T: 8 <= length ((b3 :: b5 :: b7 :: hd) ++ [b; b0; b1; b2])).
+  destruct hd. inversion Q. rewrite app_length. simpl.
+  rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r.
+  rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r.
+  rewrite <- Nat.add_0_l at 1. apply Nat.add_le_mono.
+  apply Nat.le_0_l. apply Nat.le_refl.
+
+  (* analyse finale *)
+  assert ({b8=b9} + {~ b8=b9}). apply bool_dec. destruct H7. rewrite e0 in H.
+
+  (* premier sous-cas : b8 = b9, contradiction lié à repeating_patterns *)
+      (* lemme initial *)
+  assert (forall n : nat, n mod 4 = 2 -> n mod 8 = 2 \/ n mod 8 = 6).
+  intro m. intro A.
+  assert (m mod (4*2) = m mod 4 + 4 * ((m / 4) mod 2)).
+  apply Nat.mod_mul_r; easy. rewrite A in H7.
+  rewrite <- Nat.bit0_mod in H7. replace (4*2) with 8 in H7.
+  rewrite H7.
+  destruct (Nat.testbit (m / 4) 0) ; [right | left] ; reflexivity.
+  reflexivity.
+  pose (lh := length ((b3 :: b5 :: b7 :: hd) ++ [b; b0; b1; b2])).
+  fold lh in H1. fold lh in T.
+
+  assert ({b9=b0} + {~ b9=b0}). apply bool_dec. destruct H8. rewrite e1 in H.
+  (* si centre = 8n + 2, alors les cinq premiers sont absurdes *)
+  (* si centre = 8n + 6, alors les cinq derniers sont absurdes *)
+  apply H7 in H1. destruct H1.
+    (* on commence par supposer le centre en 8n+2 : hypothèse H1 *)
+  assert (lh = 8 * (lh / 8) + lh mod 8). apply Nat.div_mod. easy.
+  rewrite H1 in H8. rewrite <- Nat.succ_pred_pos with (n := lh/8) in H8.
+  assert (lh - 8 = 8 * Nat.pred (lh / 8) + 2).
+  rewrite <- Nat.add_cancel_r with (p := 8). rewrite <- Nat.add_sub_swap.
+  rewrite Nat.add_sub. rewrite Nat.add_shuffle0. rewrite <- Nat.mul_succ_r.
+  assumption. assumption.
+  
+  assert (nth_error (tm_step (3 + (n-3))) (Nat.pred (lh/8) * 8 + 3)
+        = nth_error (tm_step (3 + (n-3))) (Nat.pred (lh/8) * 8 + 4)).
+  rewrite Nat.add_comm. rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub.
+  rewrite H. rewrite Nat.mul_comm.
+  apply eq_S in H9. symmetry in H9. rewrite <- Nat.add_1_r in H9.
+  rewrite <- Nat.add_assoc in H9. rewrite Nat.add_1_r in H9.
+  rewrite H9.
+  apply eq_S in H9. rewrite <- Nat.add_1_r in H9.
+  rewrite <- Nat.add_assoc in H9. rewrite Nat.add_1_r in H9.
+  rewrite H9. unfold lh. unfold hd'.
+
+  rewrite nth_error_app2. symmetry. rewrite nth_error_app2. rewrite Y''.
+  rewrite app_length.
+  replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))).
+  rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm.
+  rewrite Nat.add_succ_comm. rewrite <- Nat.sub_succ_l.
+  rewrite <- Nat.add_succ_r. rewrite Nat.add_sub.
+  rewrite Nat.sub_succ_l. rewrite Nat.sub_diag. reflexivity.
+  apply Nat.le_refl. unfold lh in T.
+  rewrite <- Nat.add_succ_comm. rewrite <- Nat.add_succ_comm.
+  rewrite <- Nat.add_succ_comm. rewrite app_length in T.
+  assumption. reflexivity. rewrite Y''.
+  rewrite app_length.
+  replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))).
+  rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm.
+  rewrite Nat.add_succ_comm. rewrite <- Nat.sub_succ_l.
+  rewrite <- Nat.add_succ_r. rewrite Nat.add_sub.
+  apply Nat.le_succ_diag_r. rewrite Nat.add_succ_r.
+  rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
+  rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
+  rewrite <- Nat.succ_le_mono. replace 5 with (1 + 4).
+  rewrite <- Nat.add_le_mono_r. destruct hd. inversion Q.
+  simpl. apply le_n_S. apply Nat.le_0_l. reflexivity. reflexivity.
+  rewrite Y''. rewrite app_length.
+  replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))).
+  rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm.
+  rewrite Nat.add_succ_comm. rewrite <- Nat.sub_succ_l.
+  rewrite <- Nat.add_succ_r. rewrite Nat.add_sub. apply Nat.le_refl.
+  rewrite Nat.add_succ_r. rewrite Nat.add_succ_r. rewrite Nat.add_succ_r.
+  rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono.
+  rewrite <- Nat.succ_le_mono. replace 5 with (1 + 4).
+  rewrite <- Nat.add_le_mono_r. destruct hd. inversion Q.
+  simpl. apply le_n_S. apply Nat.le_0_l. reflexivity. reflexivity.
+  apply Nat.lt_le_incl. assumption.
+  rewrite <- tm_step_repeating_patterns in H10. inversion H10.
+  simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
+  simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
+
+  rewrite Nat.mul_lt_mono_pos_l with (p := 8).
+  rewrite Nat.add_lt_mono_r with (p := 2). rewrite <- H9.
+  rewrite Nat.add_lt_mono_r with (p := 8).
+  rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub.
+  rewrite <- Nat.add_assoc. replace (2+8) with 10.
+  replace 8 with (2^3) at 1. rewrite <- Nat.pow_add_r.
+  rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap. simpl.
+  rewrite <- tm_size_power2. rewrite H'. unfold lh.
+  rewrite app_length. rewrite app_length. rewrite <- Nat.add_assoc.
+  rewrite <- Nat.add_lt_mono_l. simpl.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  apply Nat.lt_0_succ. apply Nat.le_refl.
+  apply Nat.lt_le_incl. assumption. reflexivity. reflexivity.
+  assumption. apply Nat.lt_0_succ.
+  apply Nat.div_le_mono with (c := 8) in T. rewrite Nat.div_same in T.
+  rewrite Nat.le_succ_l in T. assumption. easy. easy.
+
+  (* on change de modulo ; on travaille sur 8k+6 maintenant *)
+  (* si centre = 8n + 6, alors les cinq derniers sont absurdes *)
+  assert (lh = 8 * (lh / 8) + lh mod 8). apply Nat.div_mod. easy.
+  rewrite H1 in H8. rewrite <- Nat.pred_succ with (n := lh/8) in H8.
+  rewrite Nat.mul_pred_r in H8.
+
+  assert (lh + 8 = 8 * S (lh / 8) + 6).
+  rewrite <- Nat.add_cancel_r with (p := 8) in H8.
+  rewrite <- Nat.add_sub_swap in H8. rewrite Nat.sub_add in H8. assumption.
+  rewrite <- Nat.add_0_r at 1. apply Nat.add_le_mono.
+  assert (1 <= S (lh/8)). rewrite Nat.le_succ_l. apply Nat.lt_0_succ.
+  apply Nat.mul_le_mono_l with (p := 8) in H9.
+  rewrite Nat.mul_1_r in H9. assumption. apply Nat.le_0_l.
+  assert (1 <= S (lh/8)). rewrite Nat.le_succ_l. apply Nat.lt_0_succ.
+  apply Nat.mul_le_mono_l with (p := 8) in H9.
+  rewrite Nat.mul_1_r in H9. assumption.
+
+  assert (nth_error (tm_step (3 + (n-3))) (S (lh/8) * 8 + 3)
+        = nth_error (tm_step (3 + (n-3))) (S (lh/8) * 8 + 4)).
+  rewrite Nat.add_comm. rewrite <- Nat.add_sub_swap. rewrite Nat.add_sub.
+  rewrite Nat.add_succ_r in H9. rewrite Nat.add_succ_r in H9.
+  symmetry in H9. rewrite Nat.add_succ_r in H9. rewrite Nat.add_succ_r in H9.
+  apply Nat.succ_inj in H9. apply Nat.succ_inj in H9.
+  rewrite Nat.mul_comm in H9. rewrite H9.
+  rewrite Nat.add_succ_r in H9. symmetry in H9. rewrite Nat.add_succ_r in H9.
+  apply Nat.succ_inj in H9. rewrite <- H9. rewrite H. unfold lh. unfold hd'.
+
+  rewrite nth_error_app2. symmetry. rewrite nth_error_app2. rewrite Y''.
+  rewrite app_length.
+  replace (length (b3::b5::b7::hd)) with (S (S (S (length hd)))).
+  rewrite Nat.add_succ_comm. rewrite Nat.add_succ_comm.
+  rewrite Nat.add_succ_comm.
+  rewrite Nat.add_comm. rewrite <- Nat.add_sub_assoc.
+  rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. symmetry.
+  rewrite Nat.add_comm. rewrite <- Nat.add_sub_assoc.
+  rewrite Nat.add_sub_swap. rewrite Nat.sub_diag. reflexivity.
+  apply Nat.le_refl. rewrite <- Nat.add_0_r at 1.
+  rewrite <- Nat.add_le_mono_l. apply Nat.le_0_l. apply Nat.le_refl.
+  rewrite <- Nat.add_0_r at 1.
+  rewrite <- Nat.add_le_mono_l. apply Nat.le_0_l. reflexivity.
+
+  rewrite Y''. rewrite app_length. simpl. rewrite <- Nat.add_succ_r.
+  rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r.
+  rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_assoc.
+  rewrite <- Nat.add_le_mono_l. apply Nat.le_0_l.
+
+  rewrite Y''. rewrite app_length. simpl. rewrite <- Nat.add_succ_r.
+  rewrite <- Nat.add_succ_r. rewrite <- Nat.add_succ_r.
+  rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_assoc.
+  rewrite <- Nat.add_le_mono_l. apply Nat.le_0_l.
+  apply Nat.lt_le_incl. assumption.
+
+  rewrite <- tm_step_repeating_patterns in H10. inversion H10.
+  simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
+  simpl. rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
+
+  rewrite Nat.mul_lt_mono_pos_l with (p := 8).
+  rewrite Nat.add_lt_mono_r with (p := 6). rewrite <- H9.
+  replace (8) with (2^3) at 2. rewrite <- Nat.pow_add_r.
+  rewrite Nat.add_sub_assoc. rewrite Nat.add_sub_swap.
+  rewrite Nat.sub_diag. rewrite Nat.add_0_l.
+  rewrite <- tm_size_power2. rewrite H'. unfold lh.
+  rewrite app_length. rewrite app_length. rewrite <- Nat.add_assoc.
+  rewrite <- Nat.add_assoc.
+
+  rewrite <- Nat.add_lt_mono_l. simpl.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite <- Nat.succ_lt_mono.
+  rewrite <- Nat.succ_lt_mono. rewrite Nat.add_succ_r.
+  rewrite <- Nat.succ_lt_mono. rewrite Nat.add_succ_r.
+  apply Nat.lt_0_succ. apply Nat.le_refl.
+  apply Nat.lt_le_incl. assumption. reflexivity. apply Nat.lt_0_succ.
+
+  (* on arrive à la suite du cas b8 = b9 avec cette fois b9 = b1
+     et non plus b9 = b0 *)
+  assert (b9 = b1). destruct b9; destruct b1; destruct b0.
+  reflexivity. reflexivity. contradiction n6. reflexivity.
+  contradiction n1. reflexivity. contradiction n1. reflexivity.
+  contradiction n6. reflexivity. reflexivity. reflexivity.
+  rewrite H8 in H.
+
+  (* le premier nouveau sous cas est  lh mod 4 = 2 en H1
+              FTFT TFTF FTFT TFTF (µ de FF TT FF TT) pourquoi impossible ?
+       c'est un carré ???
+       c'est un palindrome fait avec un carré de palindrome ?
+       morphisme de FFTTFFTT   sans doute impossible (testé)
+   *)
+  
+  unfold hd' in H. destruct hd. inversion P.
+  rewrite app_removelast_last
+    with (l := (removelast (removelast (removelast (b3::b5::b7::b10::hd)))))
+         (d := false) in H.
+  pose (b11 := last (removelast (removelast
+           (removelast (b3 :: b5 :: b7 :: b10 :: hd)))) false).
+  fold b11 in H. rewrite <- app_assoc in H.
+  pose (hd'' := removelast (removelast (removelast
+          (removelast (b3 :: b5 :: b7 :: b10 :: hd))))).
+  fold hd'' in H.
+    (* proof that b11 <> b1 *)
+  assert ({b11=b1} + {~ b11=b1}). apply bool_dec. destruct H9. rewrite e1 in H.
+  assert (even (length hd'') = false).
+  replace ( hd'' ++ [b1] ++ [b1] ++ [b0] ++ [b1] ++
+    b1 :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: b0 :: b1 :: tl)
+    with (hd'' ++ [b1;b1;b0] ++ [b1;b1;b0]
+              ++ b1::b0::b0::b1::b0::b1::b1::b0::b1::tl) in H.
+  assert (odd (length [b1;b1;b0]) = true). reflexivity.
+  generalize H9. generalize H. apply tm_step_odd_prefix_square.
+  reflexivity. unfold hd'' in H9.
+  rewrite removelast_firstn_len in H9. rewrite Y'' in H9.
+  rewrite firstn_length_le in H9. simpl in H9.
+  replace (b3::b5::b7::b10::hd) with ([b3;b5;b7;b10] ++ hd) in Q.
+  rewrite app_length in Q. rewrite Nat.even_add in Q. rewrite H9 in Q.
+  inversion Q. reflexivity. rewrite Y''. apply Nat.le_pred_l.
+
+    (* proof ath b11 = b0 *)
+  assert (b11 = b0). destruct b11; destruct b1; destruct b0.
+  reflexivity. contradiction n7. reflexivity. reflexivity.
+  contradiction n1. reflexivity. contradiction n1. reflexivity.
+  reflexivity. contradiction n7. reflexivity. reflexivity.
+  rewrite H9 in H.
+
+    (* on élargit tl (adding b12 in front of tl)  *)
+  destruct tl.
+  assert (tm_step n = rev (tm_step n)
+           \/ tm_step n = map negb (rev (tm_step n))).
+  apply tm_step_rev. destruct H10; rewrite H in H10 at 2;
+  rewrite rev_app_distr in H10;
+  assert (odd 1 = true). reflexivity.
+  rewrite <- tm_step_pred with (n := n) (k := 0) in H11.
+  rewrite H10 in H11. simpl in H11. inversion H11. rewrite H13 in n1.
+  contradiction n1. reflexivity. simpl.
+  replace 2 with (2^1). rewrite <- Nat.pow_lt_mono_r_iff.
+  apply Nat.lt_succ_l in R. apply Nat.lt_succ_l in R. assumption.
+  apply Nat.lt_1_2. reflexivity.
+
+  reflexivity.
+  rewrite <- tm_step_pred with (n := n) (k := 0) in H11.
+  rewrite H10 in H11. simpl in H11. inversion H11.
+  destruct b0; destruct b1. contradiction n1. reflexivity.
+  inversion H13. inversion H13. contradiction n1. reflexivity. simpl.
+  replace 2 with (2^1). rewrite <- Nat.pow_lt_mono_r_iff.
+  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 *)
+  (* 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.
+
+  (* simplify notations *)
+  replace ( hd'' ++ [b0] ++ [b1] ++ [b0] ++ [b1] ++ b1
+    :: b0 :: b1 :: b0 :: b0 :: b1 :: b0 :: b1 :: b1 :: b0 :: b1 :: b0 :: tl)
+  with (hd'' ++ [b0;b1;b0;b1;b1;b0;b1;b0;b0;b1;b0;b1;b1;b0;b1;b0] ++ tl) in H.
+  pose (s := [b0;b1;b0;b1;b1;b0;b1;b0;b0;b1;b0;b1;b1;b0;b1;b0]). fold s in H.
+  assert (even (length hd'') = true). unfold hd''. 
+
+  rewrite removelast_firstn_len. rewrite Y''.
+  replace (pred (length (b10::hd))) with (length hd).
+  rewrite firstn_length_le. simpl in Q. rewrite Q. reflexivity.
+  rewrite Y''. apply Nat.le_succ_diag_r. reflexivity.
+
+  (* destructuring n *)
+  destruct n. inversion H0. rewrite <- tm_step_lemma in H.
+
+  (* inverting tm_morphism in tm_step n *)
+  assert (hd'' = tm_morphism (firstn (Nat.div2 (length hd'')) (tm_step n))).
+  generalize H11. generalize H. apply tm_morphism_app2.
+
+  assert (s ++ tl = tm_morphism (skipn (Nat.div2 (length hd'')) (tm_step n))).
+  generalize H11. generalize H. apply tm_morphism_app3. symmetry in H13.
+
+  assert (even (length s) = true). unfold s. reflexivity.
+  assert (s = tm_morphism (firstn (Nat.div2 (length s))
+      (skipn (Nat.div2 (length hd'')) (tm_step n)))).
+  generalize H14. generalize H13. apply tm_morphism_app2.
+
+  assert (tl = tm_morphism (skipn (Nat.div2 (length s))
+      (skipn (Nat.div2 (length hd'')) (tm_step n)))).
+  generalize H14. generalize H13. apply tm_morphism_app3.
+
+  rewrite H12 in H. rewrite H15 in H. rewrite H16 in H.
+  rewrite <- tm_morphism_app in H. rewrite <- tm_morphism_app in H.
+  rewrite <- tm_morphism_eq in H.
+
+  pose (h0 := firstn (Nat.div2 (length hd'')) (tm_step n)).
+  pose (s0 := firstn (Nat.div2 (length s))
+                 (skipn (Nat.div2 (length hd'')) (tm_step n))).
+  pose (t0 := skipn (Nat.div2 (length s))
+                 (skipn (Nat.div2 (length hd'')) (tm_step n))).
+  fold h0 in H. fold s0 in H. fold t0 in H.
+
+  (* fin de la preuve pour cette partie : morphisme impossible *)
+  assert (s0 = [b0;b0;b1;b1;b0;b0;b1;b1]). fold s0 in H15.
+  unfold s in H15. destruct s0. inversion H15.
+  destruct s0. inversion H15. destruct s0. inversion H15.
+  destruct s0. inversion H15. destruct s0; inversion H15.
+  destruct s0. inversion H15. destruct s0. inversion H15.
+  destruct s0. inversion H15. destruct s0; inversion H15.
+  inversion H15. reflexivity.
+  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.
+
+  (* fin de la preuve, on a b8 <> b9 *)
+  right.
+  split. assumption.
+  split. rewrite H4. rewrite e.
+  assert (b0 = negb b1). destruct b0; destruct b1.
+  contradiction n1. reflexivity. reflexivity. reflexivity.
+  contradiction n1. reflexivity. rewrite H7. exists b1.
+  reflexivity.
+
+  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.
+
+  (* fin de la destructuration de a, désormais trop grand
+     cf. hypothèse I *)
+  simpl in I. apply eq_add_S in I. apply eq_add_S in I.
+  apply eq_add_S in I. apply eq_add_S in I.
+  symmetry in I. apply O_S in I. contradiction I.
+Qed.