Update

thue-morse.v

@@ -1068,15 +1068,6 @@ Proof.
   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.
 
-  (*
-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)
-    <->
-    nth_error (tm_step (S n)) (k + 2^n)
-      = nth_error (tm_step (S n)) (S k + 2^n).
-   *)
-
   split.
   - induction m.
     + intros L. rewrite Nat.add_0_r. rewrite Nat.add_0_r.
@@ -1136,37 +1127,12 @@ Lemma tm_step_next_range2_neighbor' : forall (n k : nat),
 Qed.
 
 
-Lemma tm_step_next_range2_neighbor : forall (n k : nat),
-  S k < 2^n ->
-    eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false)
-    = eqb
-    (nth (k + 2^n) (tm_step (S n)) false) (nth (S k + 2^n) (tm_step (S n)) false).
-
-  - intros H1. induction m.
-    + rewrite Nat.add_0_r. rewrite Nat.add_0_r.
-
-nth_error_nth:
-  forall [A : Type] (l : list A) (n : nat) [x : A] (d : A),
-  nth_error l n = Some x -> nth n l d = x
-
-
-nth_error_nth':
-  forall [A : Type] (l : list A) [n : nat] (d : A),
-  n < length l -> nth_error l n = Some (nth n l d)
-
-
-Lemma tm_step_next_range2' :
-  forall (n k : nat) (b : bool),
-  nth_error (tm_step n) k = Some b
-    -> nth_error (tm_step (S n)) (k + 2^n) = Some (negb b).
 
 
 
 
 
-
+Lemma tm_step_add_range2_neighbor0 : forall (n m k : nat),
-
-Lemma tm_step_add_range2_neighbor : forall (n m k : nat),
   S k < 2^n ->
     eqb (nth k (tm_step n) false)
         (nth (S k) (tm_step n) false)