diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 2a050ef..760452e 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -1493,17 +1493,19 @@ Proof.
   apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W. apply Nat.lt_succ_l in W.
   assumption.
 
-  (* proof that n <> 0 *)
-  destruct n. assert (length (tm_step 0) <= length (tm_step 0)).
-  apply Nat.le_refl.
-  rewrite H in H0 at 1. rewrite app_length in H0. rewrite app_length in H0.
-  rewrite Nat.add_comm in H0. rewrite <- Nat.add_assoc in H0. simpl in H0.
-  apply Nat.le_add_le_sub_r in H0. rewrite app_length in H0.
-  rewrite rev_length in H0. rewrite <- Nat.add_assoc in H0.
-  assert (K: 1 <= length a + (length tl + length hd)).
-  rewrite Nat.le_succ_l. apply Nat.lt_lt_add_r. assumption.
-  rewrite <- Nat.sub_0_le in K. rewrite K in H0. apply Nat.le_0_r in H0.
-  rewrite H0 in Z. inversion Z.
+  assert (V: 1 < n). assert (length (tm_step n) <= length (tm_step n)).
+  apply Nat.le_refl. rewrite H in H0 at 1.
+  rewrite app_length in H0. rewrite app_length in H0.
+  rewrite Nat.add_comm in H0. rewrite <- Nat.add_assoc in H0.
+  rewrite <- Nat.add_0_r in H0. apply Nat.le_le_add_le in H0.
+  rewrite tm_size_power2 in H0. destruct n. destruct a.
+  inversion W. destruct a. inversion W. inversion H2.
+  destruct a. inversion W. inversion H2. inversion H4.
+  inversion H0. inversion H2. destruct a. inversion W.
+  destruct a. inversion W. inversion H2. destruct a. inversion W.
+  inversion H2. inversion H4. destruct n. inversion H0. inversion H2.
+  inversion H4. rewrite <- Nat.succ_lt_mono. apply Nat.lt_0_succ.
+  apply le_0_n. destruct n. inversion V.
 
   assert (J1: length hd mod 4 = 0). generalize J0. generalize W.
   generalize H. apply tm_step_palindromic_length_12_prefix.
@@ -1578,26 +1580,25 @@ Proof.
   rewrite U. replace 4 with (2*2). rewrite <- Nat.mul_assoc.
   rewrite Nat.div2_double. rewrite Nat.even_mul. reflexivity. easy. easy.
 
-  assert (I': even (length hd') = true).
-  unfold hd'. rewrite firstn_length_le. apply EVEN2. assumption.
+  assert (I': even (length hd') = true). unfold hd'. rewrite firstn_length.
+  assert (C: Nat.div2 (length hd) <= length (tm_step n)
+           \/ length (tm_step n) < Nat.div2 (length hd)).
+  apply Nat.le_gt_cases. destruct C.
+  apply Nat.min_r in H6. rewrite Nat.min_comm. rewrite H6.
+  apply EVEN2. assumption. apply Nat.lt_le_incl in H6.
+  apply Nat.min_l in H6. rewrite Nat.min_comm. rewrite H6.
+  rewrite tm_size_power2. destruct n. inversion V. inversion H8.
+  rewrite Nat.pow_succ_r. rewrite Nat.even_mul. reflexivity.
+  apply Nat.le_0_l.
+
 
 
 
 
 
 
-  assumption. easy.
-  rewrite Nat.div2_div. reflexivity. rewrite Nat.mul_comm. simpl.
-  rewrite Nat.add_0_r. reflexivity.
 
-  apply Nat.le_refl.
-  rewrite <- Nat.div_add. rewrite <- Nat.div2_div.
-  rewrite Nat.mul_comm.
 
-  rewrite Nat.div2_odd with (a := length a) at 2.
-  rewrite <- Nat.negb_even. rewrite J. simpl.
-  rewrite Nat.add_0_r. rewrite Nat.add_0_r. reflexivity. easy.
-Qed.