diff --git a/src/thue_morse2.v b/src/thue_morse2.v
index 677fb34..ce8201d 100644
--- a/src/thue_morse2.v
+++ b/src/thue_morse2.v
@@ -91,208 +91,75 @@ Qed.
    All squared factors of odd length have length 1 or 3.
 *)
 
-Lemma tm_step_factor5 : forall (n : nat) (hd a tl : list bool),
-  tm_step n = hd ++ a ++ tl -> length a = 5
-  -> a <> [ true; false; true; false; true].
-Proof.
-  intros n hd a tl. intros H I.
-
-  destruct n.
-  assert (length (tm_step 0) = length (tm_step 0)). reflexivity.
-  rewrite H in H0 at 2. simpl in H0.
-  rewrite app_length in H0. rewrite app_length in H0.
-  rewrite I in H0. rewrite Nat.add_shuffle3 in H0.
-  apply Nat.succ_inj in H0. inversion H0.
-
-  assert (even (length (tm_step (S n))) = true).
-  rewrite tm_size_power2. rewrite Nat.pow_succ_r. apply Nat.even_mul.
-  apply Nat.le_0_l.
-
-  assert (J: even (length hd) = negb (even (length tl))).
-  rewrite H in H0. rewrite app_length in H0. rewrite app_length in H0.
-  rewrite I in H0. rewrite Nat.even_add in H0. rewrite Nat.even_add in H0.
-  destruct (even (length hd)); destruct (even (length tl)).
-  inversion H0. reflexivity. reflexivity. inversion H0.
-
-  assert (K: {a=[true; false; true; false; true]}
-           + {~ a=[ true; false; true; false; true]}).
-  apply list_eq_dec. apply bool_dec. destruct K.
-
-  assert ({even (length hd) = true} + {even (length hd) <> true}).
-  apply bool_dec. destruct H1.
-
-  (* case length hd is even *)
-  rewrite e0 in J. rewrite Nat.negb_even in J.
-  destruct tl. inversion J.
-  destruct b.
-
-  assert (count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false).
-  generalize e0. generalize H. apply tm_step_count_occ.
-
-  assert (count_occ Bool.bool_dec (hd ++ a ++ [true]) true
-        = count_occ Bool.bool_dec (hd ++ a ++ [true]) false).
-  assert (even (length (hd ++ a ++ [true])) = true).
-  rewrite app_length. rewrite app_length.
-  rewrite Nat.even_add. rewrite Nat.even_add.
-  rewrite e0. rewrite e. reflexivity.
-  replace (hd ++ a ++ true :: tl) with ((hd ++ a ++ [true]) ++ tl) in H.
-  generalize H2. generalize H. apply tm_step_count_occ.
-  rewrite <- app_assoc. apply app_inv_head_iff.
-  rewrite <- app_assoc. reflexivity.
-
-  rewrite count_occ_app in H2. rewrite H1 in H2.
-  symmetry in H2.
-  rewrite count_occ_app in H2. rewrite Nat.add_cancel_l in H2.
-
-  rewrite count_occ_app in H2. rewrite count_occ_app in H2.
-  rewrite e in H2. simpl in H2. inversion H2.
-
-  replace (hd ++ a ++ false::tl)
-    with (hd ++ [true; false] ++ [true; false] ++ [true; false] ++ tl) in H.
-  apply tm_step_cubefree in H. contradiction H. reflexivity.
-  simpl. apply Nat.lt_0_2.
-
-  rewrite e. reflexivity.
-
-  (* case length hd is odd *)
-  apply not_true_is_false in n0.
-  rewrite app_removelast_last with (l := hd) (d := true) in H.
-  rewrite app_removelast_last with (l := hd) (d := true) in n0.
-  rewrite app_length in n0. simpl in n0.
-  rewrite Nat.add_1_r in n0. rewrite Nat.even_succ in n0.
-  rewrite <- Nat.negb_even in n0. rewrite negb_false_iff in n0.
-
-  destruct (last hd true).
-  rewrite <- app_assoc in H.
-  assert (count_occ Bool.bool_dec (removelast hd) true
-        = count_occ Bool.bool_dec (removelast hd) false).
-  generalize n0. generalize H. apply tm_step_count_occ.
-  replace (removelast hd ++ [true] ++ a ++ tl)
-    with ((removelast hd ++ [true; true]) ++ [false;true;false;true] ++ tl) in H.
-  assert (count_occ Bool.bool_dec (removelast hd ++ [true;true]) true
-        = count_occ Bool.bool_dec (removelast hd ++ [true;true]) false).
-  assert (even (length (removelast hd ++ [true;true])) = true).
-  rewrite app_length. rewrite Nat.even_add_even. assumption.
-  apply Nat.EvenT_Even. apply Nat.even_EvenT. reflexivity.
-  generalize H2. generalize H. apply tm_step_count_occ.
-
-  rewrite count_occ_app in H2. rewrite count_occ_app in H2.
-  rewrite H1 in H2. rewrite Nat.add_cancel_l in H2.
-  simpl in H2. inversion H2.
-
-  rewrite e. rewrite app_assoc_reverse. reflexivity.
-
-  replace ((removelast hd ++ [false]) ++ a ++ tl)
-    with (removelast hd ++ [false; true] ++ [false; true] ++ [false;true] ++ tl) in H.
-  apply tm_step_cubefree in H. contradiction H. reflexivity.
-  simpl. apply Nat.lt_0_2.
-
-  rewrite e. rewrite app_assoc_reverse. reflexivity.
-
-  assert (length hd <> 0). destruct hd. inversion n0.
-  simpl. apply Nat.neq_succ_0. rewrite <- length_zero_iff_nil. assumption.
-  assert (length hd <> 0). destruct hd. inversion n0.
-  simpl. apply Nat.neq_succ_0. rewrite <- length_zero_iff_nil. assumption.
-
-  assumption.
-Qed.
-
-Lemma tm_step_factor5' : forall (n : nat) (hd a tl : list bool),
-  tm_step n = hd ++ a ++ tl -> length a = 5
-  -> a <> [ false; true; false; true; false].
-Proof.
-  intros n hd a tl. intros H I.
-  assert (K: {a=[false; true; false; true; false]}
-           + {~ a=[false; true; false; true; false]}).
-  apply list_eq_dec. apply bool_dec. destruct K.
-  assert (tm_step (S n) = hd ++ a ++ tl
-          ++ (map negb hd) ++ [ true; false; true; false; true ]
-          ++ (map negb tl)).
-  rewrite tm_build. rewrite H.
-  rewrite map_app. rewrite map_app.
-  rewrite <- app_assoc. apply app_inv_head_iff.
-  rewrite <- app_assoc. rewrite e. reflexivity.
-  rewrite app_assoc in H0. rewrite app_assoc in H0.
-  rewrite app_assoc in H0. apply tm_step_factor5 in H0.
-  contradiction H0. reflexivity.
-  reflexivity. assumption.
-Qed.
-
-
 Lemma tm_step_consecutive_identical_length :
-  forall (n : nat) (hd a tl : list bool),
-  tm_step n = hd ++ a ++ tl -> length a = 5
-  -> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c.
-Proof.
-  intros n hd a tl. intros H I.
-  destruct a. inversion I. destruct a. inversion I.
-  destruct a. inversion I. destruct a. inversion I.
-  destruct a. inversion I.
-
-  assert (a = nil). simpl in I.
-  apply Nat.succ_inj in I. apply Nat.succ_inj in I.
-  apply Nat.succ_inj in I. apply Nat.succ_inj in I.
-  apply Nat.succ_inj in I.
-  apply length_zero_iff_nil in I. assumption.
-  rewrite H0. rewrite H0 in H. rewrite H0 in I.
-
-  destruct b; destruct b0; destruct b1; destruct b2; destruct b3.
-
-  exists nil. exists (true::true::true::nil). exists true. simpl. reflexivity.
-  exists nil. exists (true::true::false::nil). exists true. simpl. reflexivity.
-  exists nil. exists (true::false::true::nil). exists true. simpl. reflexivity.
-  exists nil. exists (true::false::false::nil). exists true. simpl. reflexivity.
-  exists nil. exists (false::true::true::nil). exists true. simpl. reflexivity.
-  exists nil. exists (false::true::false::nil). exists true. simpl. reflexivity.
-  exists nil. exists (false::false::true::nil). exists true. simpl. reflexivity.
-  exists nil. exists (false::false::false::nil). exists true. simpl. reflexivity.
-
-  exists (true::false::nil). exists (true::nil). exists true. simpl. reflexivity.
-  exists (true::false::nil). exists (false::nil). exists true. simpl. reflexivity.
-  apply tm_step_factor5 in H. contradiction H. reflexivity. reflexivity.
-  exists (true::false::true::nil). exists (nil). exists false. simpl. reflexivity.
-  exists (true::false::false::nil). exists (nil). exists true. simpl. reflexivity.
-  exists (true::nil). exists (true::false::nil). exists false. simpl. reflexivity.
-  exists (true::nil). exists (false::true::nil). exists false. simpl. reflexivity.
-  exists (true::false::nil). exists (false::nil). exists false. simpl. reflexivity.
-  exists (false::nil). exists (true::true::nil). exists true. simpl. reflexivity.
-  exists (false::nil). exists (true::false::nil). exists true. simpl. reflexivity.
-  exists (false::nil). exists (false::true::nil). exists true. simpl. reflexivity.
-  exists (false::nil). exists (false::false::nil). exists true. simpl. reflexivity.
-  exists (false::true::false::nil). exists (nil). exists true. simpl. reflexivity.
-  apply tm_step_factor5' in H. contradiction H. reflexivity. reflexivity.
-  exists (false::true::nil). exists (true::nil). exists false. simpl. reflexivity.
-  exists (false::true::nil). exists (false::nil). exists false. simpl. reflexivity.
-  exists (false::false::nil). exists (true::nil). exists true. simpl. reflexivity.
-  exists (false::false::nil). exists (false::nil). exists true. simpl. reflexivity.
-  exists (nil). exists (true::false::true::nil). exists false. simpl. reflexivity.
-  exists (nil). exists (true::false::false::nil). exists false. simpl. reflexivity.
-  exists (nil). exists (false::true::true::nil). exists false. simpl. reflexivity.
-  exists (nil). exists (false::true::false::nil). exists false. simpl. reflexivity.
-  exists (nil). exists (false::false::true::nil). exists false. simpl. reflexivity.
-  exists (nil). exists (false::false::false::nil). exists false. simpl. reflexivity.
-Qed.
-
-Lemma tm_step_consecutive_identical_length' :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ tl -> 4 < length a
   -> exists (b c : list bool) (d : bool), a = b ++ [d;d] ++ c.
 Proof.
   intros n hd a tl. intros H I.
-  rewrite <- firstn_skipn with (l := a) (n := 5).
-  assert (length (firstn 5 a) = 5).
-  apply firstn_length_le. apply Nat.le_succ_l. apply I.
-  rewrite <- firstn_skipn with (l := a) (n := 5) in H.
-  rewrite <- app_assoc in H.
-  assert (exists (b1 c1 : list bool) (d1 : bool),
-    firstn 5 a = b1 ++ [d1; d1] ++ c1).
-  generalize H0. generalize H. apply tm_step_consecutive_identical_length.
-  destruct H1. destruct H1. destruct H1. rewrite H1.
-  exists x. exists (x0 ++ (skipn 5 a)). exists x1.
-  rewrite <- app_assoc. apply app_inv_head_iff.
-  rewrite <- app_assoc. reflexivity.
-Qed.
+  assert (J: Nat.Even (length hd) \/ Nat.Odd (length hd)).
+  apply Nat.Even_or_Odd. destruct J as [J | J].
 
+  (* first case *)
+  replace (hd++a++tl)
+    with ((hd ++ (firstn 1 a)) ++ (skipn 1 (firstn 5 a))
+                               ++ ((skipn 5 a) ++ tl)) in H.
+
+  assert (length (skipn 1 (firstn 5 a)) = 4).
+  rewrite skipn_length. rewrite firstn_length.
+  rewrite <- Nat.le_succ_l in I. rewrite Nat.min_l.
+  reflexivity. assumption.
+
+  assert (odd (length (hd ++ firstn 1 a)) = true).
+  rewrite app_length. rewrite Nat.odd_add. rewrite <- Nat.negb_even.
+  apply Nat.Even_EvenT in J. apply Nat.EvenT_even in J. rewrite J.
+  rewrite firstn_length. rewrite Nat.min_l. reflexivity.
+  
+  apply Nat.lt_le_incl.
+  assert (1 < 4). rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
+  generalize I. generalize H1. apply Nat.lt_trans.
+
+  assert (exists (x : bool) (u v : list bool),
+    skipn 1 (firstn 5 a) = u ++ [x;x] ++ v).
+  generalize H1. generalize H0. generalize H. apply tm_step_pattern4_odd_prefix.
+  destruct H2. destruct H2. destruct H2.
+  exists ((firstn 1 a) ++ x0). exists (x1 ++ (skipn 5 a)). exists x.
+  replace ((firstn 1 a ++ x0) ++ [x; x] ++ x1 ++ skipn 5 a)
+    with (firstn 1 a ++ (x0 ++ [x;x] ++ x1) ++ skipn 5 a). rewrite <- H2.
+  rewrite app_assoc. replace (firstn 1 a) with (firstn 1 (firstn 5 a)).
+  rewrite firstn_skipn. rewrite firstn_skipn. reflexivity.
+  rewrite firstn_firstn. reflexivity.
+  rewrite <- app_assoc. rewrite <- app_assoc. rewrite <- app_assoc.
+  reflexivity.
+  rewrite <- app_assoc. apply app_inv_head_iff.
+  replace (firstn 1 a) with (firstn 1 (firstn 5 a)).
+  rewrite app_assoc. rewrite firstn_skipn.
+  rewrite app_assoc. rewrite firstn_skipn.
+  reflexivity.
+  rewrite firstn_firstn. reflexivity.
+
+  (* second case *)
+  replace (hd++a++tl) with (hd ++ (firstn 4 a) ++ ((skipn 4 a) ++ tl)) in H.
+
+  assert (length (firstn 4 a) = 4). rewrite firstn_length.
+  rewrite <- Nat.le_succ_l in I. rewrite Nat.min_l.
+  reflexivity. assert (4 <= 5). apply Nat.le_succ_diag_r.
+  generalize I. generalize H0. apply Nat.le_trans.
+
+  apply Nat.Odd_OddT in J. apply Nat.OddT_odd in J.
+
+  assert (exists (x : bool) (u v : list bool), firstn 4 a = u ++ [x;x] ++ v).
+  generalize J. generalize H0. generalize H. apply tm_step_pattern4_odd_prefix.
+  destruct H1. destruct H1. destruct H1.
+  exists x0. exists (x1++(skipn 4 a)). exists x.
+
+  replace (x0 ++ [x;x] ++ x1 ++ (skipn 4 a))
+  with ((x0++[x;x]++x1) ++ (skipn 4 a)).
+  rewrite <- H1. rewrite firstn_skipn. reflexivity.
+  rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
+  apply app_inv_head_iff.
+  rewrite app_assoc. rewrite firstn_skipn. reflexivity.
+Qed.
 
 Theorem tm_step_odd_square : forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ a ++ tl -> odd (length a) = true -> length a < 4.
@@ -301,7 +168,7 @@ Proof.
   assert (J: 4 < length a \/ length a <= 4).
   apply Nat.lt_ge_cases. destruct J.
   assert (exists b c d, a = b ++ [d;d] ++ c).
-  generalize H0. generalize H. apply tm_step_consecutive_identical_length'.
+  generalize H0. generalize H. apply tm_step_consecutive_identical_length.
   destruct H1. destruct H1. destruct H1. rewrite H1 in H.
 
   replace (hd ++ (x ++ [x1; x1] ++ x0) ++ (x ++ [x1; x1] ++ x0) ++ tl)
@@ -829,7 +696,3 @@ Proof.
     (* TODO: utiliser tm_step_odd_prefix_square pour le cas impair *)
     (* TODO: la taille du facteur divise la taille du préfixe ? *)
 
-Admitted.
-
-
-