diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 9e0c467..9479d76 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -1556,7 +1556,9 @@ Lemma tm_step_palindromic_even_morphism2 :
      /\ a = tm_morphism (tm_morphism
            (firstn (length a / 4) (skipn (length hd / 4)
            (tm_step (pred (pred n))))))
-     /\ 11 = 42.
+     /\ tl = tm_morphism (tm_morphism
+           (skipn (length hd / 4 + Nat.div2 (length a))
+             (tm_step (pred (pred n))))).
 Proof.
   intros n hd a tl. intros H W J0.
 
@@ -1809,10 +1811,26 @@ Proof.
   apply Nat.le_add_le_sub_l.
   rewrite <- H6. rewrite <- H7. assumption.
 
-
-
-Nat.div2 (length hd) + Nat.div2 (length a) <= length (tm_step (S n))
-
+  rewrite <- pred_Sn. rewrite <- pred_Sn. rewrite H3.
+  rewrite app_length.
+  rewrite app_length. rewrite rev_length.
+  replace (length a + length a) with (length a * 2).
+  rewrite Nat.div2_div. rewrite Nat.div_add.
+  rewrite <- Nat.div2_div. fold tl'. rewrite H3'.
+  rewrite app_length.
+  rewrite app_length. rewrite map_length. rewrite rev_length.
+  replace (length a' + length a') with (length a' * 2).
+  rewrite Nat.div2_div. rewrite Nat.div_add.
+  rewrite H6. rewrite H7.
+  rewrite Nat.div2_div. rewrite Nat.div_div. reflexivity.
+  easy. easy. easy.
+  rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
+  easy.
+  rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
+  easy.
+  rewrite Nat.div2_div. reflexivity.
+  rewrite Nat.mul_comm. simpl. rewrite Nat.add_0_r. reflexivity.
+  apply Nat.le_refl.
 
 
 Admitted.
@@ -1839,7 +1857,6 @@ Admitted.
 
 
 
-
 
 
 Lemma tm_step_proper_palindromic_center :