diff --git a/thue-morse.v b/thue-morse.v
index 9d9b1e4..1cbdc53 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -42,6 +42,40 @@ Proof.
     reflexivity. rewrite negb_involutive. reflexivity.
 Qed.
 
+Lemma lt_split_bits : forall n m k j,
+  0 < k -> j < 2^m -> k*2^m < 2^n -> k*2^m+j < 2^n.
+Proof.
+  intros n m k j. intros H I J.
+
+  assert (K: 2^m <= k*2^m). rewrite <- Nat.mul_1_l at 1.
+  apply Nat.mul_le_mono_r. rewrite Nat.le_succ_l. assumption.
+
+  assert (L:2^m < 2^n). generalize J. generalize K. apply Nat.le_lt_trans.
+
+  assert (k < 2^(n-m)). rewrite Nat.mul_lt_mono_pos_r with (p := 2^m).
+  rewrite <- Nat.pow_add_r. rewrite Nat.sub_add. assumption.
+  apply Nat.pow_lt_mono_r_iff in L. apply Nat.lt_le_incl. assumption.
+  apply Nat.lt_1_2. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+
+  replace (2^(n-m)) with (S (2^(n-m)-1)) in H0. rewrite Nat.lt_succ_r in H0.
+  apply Nat.mul_le_mono_r with (p := 2^m) in H0.
+  rewrite Nat.mul_sub_distr_r in H0. rewrite Nat.mul_1_l in H0.
+  rewrite <- Nat.pow_add_r in H0. rewrite Nat.sub_add in H0.
+
+  rewrite Nat.add_le_mono_r with (p := j) in H0.
+  assert (2^n - 2^m + j < 2^n).
+  rewrite Nat.add_lt_mono_l with (p := 2^n) in I.
+  rewrite Nat.add_lt_mono_r with (p := 2^m).
+  rewrite <- Nat.add_assoc. rewrite <- Nat.add_sub_swap.
+  rewrite Nat.add_assoc. rewrite Nat.add_sub. assumption.
+
+  apply Nat.lt_le_incl. assumption.
+  generalize H1. generalize H0. apply Nat.le_lt_trans.
+  apply Nat.lt_le_incl. rewrite <- Nat.pow_lt_mono_r_iff in L. assumption.
+  apply Nat.lt_1_2. rewrite <- Nat.add_1_r. apply Nat.sub_add.
+  rewrite Nat.le_succ_l. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+Qed.
+
 Lemma tm_morphism_concat : forall (l1 l2 : list bool),
   tm_morphism (l1 ++ l2) = tm_morphism l1 ++ tm_morphism l2.
 Proof.
@@ -423,40 +457,6 @@ Proof.
       apply H1. apply H2.
 Qed.
 
-Lemma lt_split_bits : forall n m k j,
-  0 < k -> j < 2^m -> k*2^m < 2^n -> k*2^m+j < 2^n.
-Proof.
-  intros n m k j. intros H I J.
-
-  assert (K: 2^m <= k*2^m). rewrite <- Nat.mul_1_l at 1.
-  apply Nat.mul_le_mono_r. rewrite Nat.le_succ_l. assumption.
-
-  assert (L:2^m < 2^n). generalize J. generalize K. apply Nat.le_lt_trans.
-
-  assert (k < 2^(n-m)). rewrite Nat.mul_lt_mono_pos_r with (p := 2^m).
-  rewrite <- Nat.pow_add_r. rewrite Nat.sub_add. assumption.
-  apply Nat.pow_lt_mono_r_iff in L. apply Nat.lt_le_incl. assumption.
-  apply Nat.lt_1_2. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
-
-  replace (2^(n-m)) with (S (2^(n-m)-1)) in H0. rewrite Nat.lt_succ_r in H0.
-  apply Nat.mul_le_mono_r with (p := 2^m) in H0.
-  rewrite Nat.mul_sub_distr_r in H0. rewrite Nat.mul_1_l in H0.
-  rewrite <- Nat.pow_add_r in H0. rewrite Nat.sub_add in H0.
-
-  rewrite Nat.add_le_mono_r with (p := j) in H0.
-  assert (2^n - 2^m + j < 2^n).
-  rewrite Nat.add_lt_mono_l with (p := 2^n) in I.
-  rewrite Nat.add_lt_mono_r with (p := 2^m).
-  rewrite <- Nat.add_assoc. rewrite <- Nat.add_sub_swap.
-  rewrite Nat.add_assoc. rewrite Nat.add_sub. assumption.
-
-  apply Nat.lt_le_incl. assumption.
-  generalize H1. generalize H0. apply Nat.le_lt_trans.
-  apply Nat.lt_le_incl. rewrite <- Nat.pow_lt_mono_r_iff in L. assumption.
-  apply Nat.lt_1_2. rewrite <- Nat.add_1_r. apply Nat.sub_add.
-  rewrite Nat.le_succ_l. rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
-Qed.
-
 Lemma tm_step_repeating_patterns :
   forall (n m i j : nat),
   i < 2^m -> j < 2^m
@@ -614,7 +614,7 @@ Proof.
   generalize P. generalize I. apply Nat.lt_le_trans.
 Qed.
 
-Lemma tm_step_succ_double_index : forall (n k : nat),
+Theorem tm_step_succ_double_index : forall (n k : nat),
   k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (S (2*k)).
 Proof.
   intros n k. intro H. rewrite tm_step_double_index.