diff --git a/thue-morse.v b/thue-morse.v
index e14e265..79200e7 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -1300,13 +1300,12 @@ Proof.
    simpl. rewrite <- Nat.succ_le_mono. rewrite <- Nat.succ_le_mono. apply Nat.le_0_l.
    assert (length (b++b++b++tl2) = 2 * length (skipn (Nat.div2 (length hd2)) (tm_step n))).
    rewrite M. apply tm_morphism_size.
-   assert (6 <= length (b++b++b++tl2)).
-   rewrite app_length. replace (6) with (2+4). apply Nat.add_le_mono. assumption.
-   rewrite app_length. replace (4) with (2+2). apply Nat.add_le_mono. assumption.
-   rewrite app_length. replace (2) with (2+0). apply Nat.add_le_mono. assumption.
-   apply Nat.le_0_l. apply Nat.add_0_r. easy. easy.
-   rewrite H3 in H4. replace (6) with (2*3) in H4. rewrite <- Nat.mul_le_mono_pos_l in H4.
 
+   assert (2 <= length (b++b++b++tl2)).
+   rewrite app_length. replace (2) with (2+0). apply Nat.add_le_mono. assumption.
+   apply Nat.le_0_l. apply Nat.add_0_r.
+   rewrite H3 in H4. replace (2) with (2*1) in H4. rewrite <- Nat.mul_le_mono_pos_l in H4.
+    
    rewrite firstn_length. rewrite <- Nat.le_succ_l.
    assert (1 <= Nat.div2 (length b)).
    rewrite Nat.mul_le_mono_pos_l with (p:= 2). rewrite Nat.mul_1_r.
@@ -1314,14 +1313,16 @@ Proof.
    rewrite <- Nat.div2_odd. assumption.
    rewrite <- Nat.negb_even. rewrite J. simpl. rewrite Nat.add_0_r. reflexivity.
    apply Nat.lt_0_2.
-   assert (1 <= 3). rewrite <- Nat.succ_le_mono. apply Nat.le_0_l.
-   assert (1 <= length (skipn (Nat.div2 (length hd2)) (tm_step n))).
-   generalize H4. generalize H6. apply Nat.le_trans.
-   generalize H7. generalize H5. apply Nat.min_glb.
+   generalize H4. generalize H5. apply Nat.min_glb.
    apply Nat.lt_0_2. easy.
 Qed.
 
 
+Theorem tm_step_cubefree : forall (n : nat) (hd a b tl : list bool),
+  tm_step n = hd ++ a ++ a ++ b ++ tl -> a <> b.
+Proof.
+  intros n hd a b tl. intro H.
+  assert (I: a=b \/ a<>b).