Update

thue-morse.v

@@ -974,16 +974,30 @@ 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)
     = eqb
-    (nth (k + 2^n) (tm_step (n+m)) false) (nth (S k + 2^n) (tm_step (n+m)) false).
+    (nth (k + 2^n) (tm_step (S n+m)) false) (nth (S k + 2^n) (tm_step (S n+m)) false).
 Proof.
-
+  intros n m k. intros H.
-
+  induction m.
-
+  - rewrite Nat.add_0_r. generalize H. apply tm_step_next_range2_neighbor.
-
+  - rewrite Nat.add_succ_r. 
-nth_error_nth':
+    assert (I : 
-  forall [A : Type] (l : list A) [n : nat] (d : A),
+      eqb (nth (k + 2 ^ n) (tm_step (S n + m)) false)
-  n < length l -> nth_error l n = Some (nth n l d)
+        (nth (S k + 2 ^ n) (tm_step (S n + m)) false)
-
+        =
+eqb (nth (k + 2 ^ n) (tm_step (S (S n + m))) false)
+  (nth (S k + 2 ^ n) (tm_step (S (S n + m))) false)
+  ).
+  assert (S k < 2^(S n + m)).
+  induction m.
+  + rewrite Nat.add_0_r. simpl. generalize H.
+    apply Nat.lt_lt_add_r.
+  + assert (2^n < 2^(S n + S m)).
+    assert (n < S n + S m). rewrite Nat.add_succ_comm.
+    apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
+    generalize H0. assert (1 < 2). apply Nat.lt_1_2. generalize H1.
+    apply Nat.pow_lt_mono_r. generalize H0. generalize H.
+    apply Nat.lt_trans.
+  +