diff --git a/thue-morse.v b/thue-morse.v
index 26b4b3c..d05a9d9 100644
--- a/thue-morse.v
+++ b/thue-morse.v
@@ -839,7 +839,7 @@ Proof.
   apply Nat.lt_0_succ.
 Qed.
 
-Lemma tm_step_next_range' :
+Lemma tm_step_next_range :
   forall (n k : nat) (b : bool),
   nth_error (tm_step n) k = Some b -> nth_error (tm_step (S n)) k = Some b.
 Proof.
@@ -860,7 +860,7 @@ Proof.
     generalize H. apply nth_error_nth'.
     rewrite H0 in IHm. symmetry in IHm.
     rewrite H0. symmetry. generalize IHm.
-    apply tm_step_next_range'.
+    apply tm_step_next_range.
 Qed.
 
 Theorem tm_step_stable : forall (n m k : nat),
@@ -885,7 +885,7 @@ Proof.
     reflexivity.
 Qed.
 
-Lemma tm_step_next_range2'' :
+Lemma tm_step_next_range2 :
   forall (n k : nat),
   k < 2^n -> nth_error (tm_step n) k <> nth_error (tm_step (S n)) (k + 2^n).
 Proof.
@@ -902,7 +902,7 @@ Proof.
   rewrite tm_size_power2. apply Nat.le_add_l.
 Qed.
 
-Lemma tm_step_next_range2_neighbor' : forall (n k : nat),
+Lemma tm_step_next_range2_neighbor : forall (n k : nat),
   S k < 2^n ->
     nth_error (tm_step n) k = nth_error (tm_step n) (S k)
     <->
@@ -913,9 +913,9 @@ Proof.
   (* 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''.
+  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''.
+  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.
@@ -986,13 +986,13 @@ Proof.
   split.
   - induction m.
     + intros L. rewrite Nat.add_0_r. rewrite Nat.add_0_r.
-    apply tm_step_next_range2_neighbor'. rewrite <- Nat.add_succ_l.
+    apply tm_step_next_range2_neighbor. rewrite <- Nat.add_succ_l.
     apply K.
-    rewrite <- tm_step_next_range2_neighbor'.
-    apply tm_step_next_range2_neighbor'. rewrite <- Nat.add_succ_l.
+    rewrite <- tm_step_next_range2_neighbor.
+    apply tm_step_next_range2_neighbor. rewrite <- Nat.add_succ_l.
     apply K.
-    rewrite <- tm_step_next_range2_neighbor'. rewrite <- Nat.add_succ_l.
-    rewrite <- tm_step_next_range2_neighbor'. apply L.
+    rewrite <- tm_step_next_range2_neighbor. rewrite <- Nat.add_succ_l.
+    rewrite <- tm_step_next_range2_neighbor. apply L.
     apply H. rewrite <- Nat.add_succ_l. apply K.
     rewrite <- Nat.add_succ_l. apply K.
     + intros L.
@@ -1007,7 +1007,7 @@ Proof.
       generalize H0. generalize H. apply Nat.lt_trans.
       assert (H1 := H0). apply Nat.lt_succ_l in H1.
 
-      rewrite <- tm_step_next_range2_neighbor'.
+      rewrite <- tm_step_next_range2_neighbor.
 
       assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k).
       generalize H1. generalize I. apply tm_step_stable.
@@ -1018,7 +1018,7 @@ Proof.
       apply H0.
   - induction m.
     + intros L. rewrite Nat.add_0_r in L. rewrite Nat.add_0_r in L.
-      apply tm_step_next_range2_neighbor'. apply H. apply L.
+      apply tm_step_next_range2_neighbor. apply H. apply L.
     + intros L.
       rewrite Nat.add_succ_r in L. rewrite Nat.add_succ_r in L.
 
@@ -1030,7 +1030,7 @@ Proof.
       generalize H0. generalize H. apply Nat.lt_trans.
       assert (H1 := H0). apply Nat.lt_succ_l in H1.
 
-      rewrite <- tm_step_next_range2_neighbor' in L.
+      rewrite <- tm_step_next_range2_neighbor in L.
 
       assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k).
       generalize H1. generalize I. apply tm_step_stable.