diff --git a/thue-morse.v b/thue-morse.v
index c491a63..84e3486 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -994,14 +994,65 @@ Lemma tm_step_next_range2_neighbor' : forall (n k : nat),
     nth_error (tm_step (S n)) (k + 2^n)
       = nth_error (tm_step (S n)) (S k + 2^n).
 Proof.
+  intros n k. intros H.
+  (* Part 1: preamble *)
+  assert (I := H). apply Nat.lt_succ_l in I.
+  assert (nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n)).
+  generalize I. apply tm_step_next_range2''.
+  assert (nth_error (tm_step n) (S k) <> nth_error (tm_step (S n)) (S k + 2^n)).
+  generalize H. apply tm_step_next_range2''.
+  assert (K: S k + 2^n < 2^(S n)). simpl. rewrite Nat.add_0_r.
+  rewrite <- Nat.add_succ_l. rewrite <- Nat.add_lt_mono_r. apply H.
+  assert (J := K). rewrite Nat.add_succ_l in J. apply Nat.lt_succ_l in J.
 
+  (* Part 2 *)
+  assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
+  generalize I. rewrite <- tm_size_power2. apply nth_error_nth'.
+  assert (nth_error (tm_step n) (S k) = Some (nth (S k) (tm_step n) false)).
+  generalize H. rewrite <- tm_size_power2. apply nth_error_nth'.
+  assert (nth_error (tm_step (S n)) (k + 2 ^ n) =
+    Some (nth (k + 2^n) (tm_step (S n)) false)).
+  generalize J. rewrite <- tm_size_power2. rewrite <- tm_size_power2.
+  apply nth_error_nth'.
+  assert (nth_error (tm_step (S n)) (S k + 2 ^ n) =
+    Some (nth (S k + 2^n) (tm_step (S n)) false)).
+  generalize K. rewrite <- tm_size_power2. rewrite <- tm_size_power2.
+  apply nth_error_nth'.
+  rewrite H2. rewrite H3. rewrite H4. rewrite H5.
 
-
-
-
-
-
-
+  (* Part 3 *)
+  destruct (nth k (tm_step n) false).
+  destruct (nth (S k) (tm_step n) false).
+  destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
+  destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
+  easy.
+  rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
+  destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
+  rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
+  easy.
+  destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
+  destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
+  rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
+  easy.
+  destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
+  easy.
+  rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
+  destruct (nth (S k) (tm_step n) false).
+  destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
+  destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
+  rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
+  easy.
+  destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
+  easy.
+  rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
+  destruct (nth (k + 2 ^ n) (tm_step (S n)) false).
+  destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
+  easy.
+  rewrite H3 in H1. rewrite H5 in H1. contradiction H1. reflexivity.
+  destruct (nth (S k + 2 ^ n) (tm_step (S n)) false).
+  rewrite H2 in H0. rewrite H4 in H0. contradiction H0. reflexivity.
+  easy.
+Qed.
 
 
 Lemma tm_step_add_range2_neighbor : forall (n m k : nat),