diff --git a/src/thue_morse4.v b/src/thue_morse4.v
index 646f8c0..afc8c92 100644
--- a/src/thue_morse4.v
+++ b/src/thue_morse4.v
@@ -1445,7 +1445,7 @@ Proof.
     rewrite Nat.pow_succ_r; lia || rewrite Nat.pow_succ_r; lia.
 Qed.
 
-Lemma tm_step_square_rev_even' :
+Lemma tm_step_square2_rev_even :
   forall (m n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ a ++ tl
   -> length a = 2^m
@@ -1524,7 +1524,7 @@ Proof.
   assumption. lia. lia.
 Qed.
 
-Lemma tm_step_square_rev_even_swap :
+Lemma tm_step_square2_rev_even_swap :
   forall (m n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ a ++ tl
   -> length a = 2^m
@@ -1559,7 +1559,7 @@ Proof.
   apply tm_step_square_rev_even.
 Qed.
 
-Lemma tm_step_square_even_pos :
+Lemma tm_step_square2_even_pos :
   forall (m n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ a ++ tl
   -> length a = 2^m
@@ -1568,14 +1568,14 @@ Lemma tm_step_square_even_pos :
 Proof.
   intros m n hd a tl. intros H I J.
   assert (a = rev a).
-  rewrite tm_step_square_rev_even_swap
+  rewrite tm_step_square2_rev_even_swap
     with (n := n) (hd := hd) (a := a) (tl := tl) (m := m) in J; assumption.
   generalize H0. generalize I. generalize H.
-  apply tm_step_square_rev_even'.
+  apply tm_step_square2_rev_even.
 Qed.
 
 
-Lemma tm_step_square_rev_odd_swap :
+Lemma tm_step_square3_rev_even_swap :
   forall (m n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ a ++ tl
   -> length a = 3*2^m
@@ -1647,26 +1647,108 @@ Lemma tm_step_square3_rev_even :
   tm_step n = hd ++ a ++ a ++ tl
   -> length a = 3 * 2^m
   -> a = rev a
-  -> 11 = 11.
+  -> length (hd ++ a) mod 2^(S m) = 0.
 Proof.
   intros m n hd a tl. intros H I J.
 
+  assert (even m = true).
+  rewrite <- tm_step_square3_rev_even_swap
+    with (n := n) (hd := hd) (a := a) (tl := tl) (m := m) in J; assumption.
 
-  assert (
-     skipn (length (hd ++ a) - 2^(S (Nat.log2 (length a)))) (hd ++ a)
-    = rev (firstn (2^S (Nat.log2 (length a))) (a ++ tl))
-      /\ 2^(S (Nat.log2 (length a))) <= length (hd ++ a)
-      /\ 2^(S (Nat.log2 (length a))) <= length (a ++ tl)).
-  generalize H0. generalize H. apply tm_step_square_even_rev'_alpha.
-  destruct H1. rewrite I in H1. rewrite Nat.log2_pow2 in H1.
-  rewrite I in H2. rewrite Nat.log2_pow2 in H2.
+  destruct m.
+  assert (even (length (hd ++ a)) = true).
+  assert (0 < length a). destruct a. inversion I.
+  simpl. lia. generalize H1. generalize H. apply tm_step_square_pos.
+  apply Nat.even_EvenT in H1. apply Nat.EvenT_Even in H1.
+  apply Nat.Even_double in H1. rewrite H1. rewrite Nat.double_twice.
+  rewrite Nat.mul_comm. apply Nat.mod_mul. easy.
 
+  destruct m. inversion H0.
 
-Lemma tm_step_square_even_rev'_alpha :
-  forall (j n : nat) (hd a tl : list bool),
-  tm_step n = hd ++ a ++ a ++ tl
-  -> length a = 2^(Nat.double j) \/ length a = 3 * 2^(Nat.double j)
-  -> skipn (length (hd ++ a) - 2^(S (Nat.log2 (length a)))) (hd ++ a)
-    = rev (firstn (2^S (Nat.log2 (length a))) (a ++ tl))
-      /\ 2^(S (Nat.log2 (length a))) <= length (hd ++ a)
-      /\ 2^(S (Nat.log2 (length a))) <= length (a ++ tl).
+  rewrite app_assoc in H.
+  rewrite <- firstn_skipn with (l := hd ++ a)
+         (n := length (hd++a) - 2^(S (S (S m)))) in H.
+  rewrite <- firstn_skipn with (l := a ++ tl) (n := 2^(S (S (S m)))) in H.
+  rewrite <- firstn_skipn with (l := a)
+                 (n := length (a) - 2^(S (S (S m)))) in J at 1.
+  rewrite <- firstn_skipn with (l := a)
+                 (n := 2^(S (S (S m)))) in J at 5.
+
+  rewrite skipn_app in H. rewrite skipn_all2 in H.
+  replace (firstn (2^(S (S (S m)))) (a++tl))
+    with (firstn (2^(S (S (S m)))) a
+          ++ firstn (2^(S (S (S m))) - length a) tl) in H.
+
+  rewrite rev_app_distr in J. assert (J' := J).
+  apply app_eq_length_head in J.
+  rewrite J in J'. apply app_inv_head in J'.
+
+  rewrite app_nil_l in H.
+  replace (length (hd ++ a) - 2 ^ (S (S (S m))) - length hd)
+    with (length a - 2^(S (S (S m)))) in H.
+  assert (firstn (2^(S (S (S m)))) a
+          = rev (skipn (length a - 2^(S (S (S m)))) a)).
+  rewrite J'. rewrite rev_involutive. reflexivity. rewrite H1 in H.
+
+  assert (length (skipn (length a - 2^(S (S (S m)))) a)
+       = 2^(S (Nat.double (Nat.div2 (S (S m)))))).
+  rewrite skipn_length.
+  replace (length a) with ((length a - 2^(S (S (S m)))) + 2^(S (S (S m)))) at 1.
+  rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
+  rewrite <- Nat.Even_double. reflexivity.
+  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
+  apply Nat.le_refl. apply Nat.sub_add. rewrite I.
+  rewrite Nat.pow_succ_r. apply Nat.mul_le_mono_r. lia. lia.
+
+  assert (6 < length (skipn (length a - 2^(S (S (S m)))) a)).
+  rewrite skipn_length.
+  replace (length a) with ((length a - 2^(S (S (S m)))) + 2^(S (S (S m)))) at 1.
+  rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
+  rewrite Nat.add_0_l. rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r.
+  rewrite Nat.pow_succ_r. rewrite Nat.mul_assoc. rewrite Nat.mul_assoc.
+  replace (2*2*2) with 8.
+  assert (6 < 8). lia. assert (8 <= 8*2^m).
+  rewrite <- Nat.mul_1_r at 1. apply Nat.mul_le_mono_pos_l. lia.
+  apply Nat.le_succ_l.
+  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+  generalize H4. generalize H3. apply Nat.lt_le_trans. reflexivity.
+  lia. lia. lia. lia. apply Nat.sub_add. rewrite I.
+  rewrite Nat.pow_succ_r. apply Nat.mul_le_mono_r. lia. lia.
+  
+  assert (length 
+    (firstn (length (hd ++ a) - 2 ^ S (S (S m))) (hd ++ a) ++
+     skipn (length a - 2 ^ S (S (S m))) a) mod 
+     (2 ^ S (Nat.double (Nat.div2 (S (S m))))) = 0).
+  generalize H2. generalize H3.
+  rewrite <- app_assoc in H. rewrite <- app_assoc in H. generalize H.
+  apply tm_step_palindromic_power2_odd.
+  rewrite <- Nat.Even_double in H4.
+  rewrite app_length in H4. rewrite <- Nat.add_mod_idemp_r in H4.
+  replace (
+      length (skipn (length a - 2 ^ S (S (S m))) a) mod 2 ^ S (S (S m))
+      ) with (2^(S (S (S m))) mod (2^(S (S (S m))))) in H4.
+  rewrite Nat.add_mod_idemp_r in H4. rewrite firstn_length_le in H4.
+  rewrite Nat.sub_add in H4. assumption.
+
+  rewrite app_length. rewrite I. replace 3 with (1+2).
+  rewrite Nat.mul_add_distr_r. rewrite Nat.add_assoc.
+  rewrite <- Nat.pow_succ_r. apply Nat.le_add_l. lia. reflexivity.
+  lia. apply Nat.pow_nonzero. easy. rewrite Nat.mod_same.
+  rewrite skipn_length.
+  replace (length a) with ((length a - 2^(S (S (S m)))) + 2^(S (S (S m)))) at 1.
+  rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
+  rewrite Nat.mod_same. reflexivity.
+  apply Nat.pow_nonzero. easy. apply Nat.le_refl. rewrite Nat.sub_add.
+  reflexivity. rewrite I. replace 3 with (1+2).
+  rewrite Nat.mul_add_distr_r.
+  rewrite <- Nat.pow_succ_r. apply Nat.le_add_l. lia. reflexivity.
+  apply Nat.pow_nonzero. easy.
+  apply Nat.pow_nonzero. easy.
+  apply Nat.EvenT_Even. apply Nat.even_EvenT. assumption.
+  rewrite <- Nat.sub_add_distr. rewrite Nat.add_comm.
+  rewrite Nat.sub_add_distr.
+  rewrite app_length. rewrite Nat.add_sub_swap. rewrite Nat.sub_diag.
+  reflexivity. apply Nat.le_refl.
+  rewrite rev_length. rewrite firstn_length_le.
+  rewrite skipn_length. reflexivity. apply Nat.le_sub_l.
+  rewrite <- firstn_app. reflexivity.