Update

thue-morse.v

@@ -1376,26 +1376,32 @@ Proof.
   rewrite nth_error_nth' with (d := false). easy.
   rewrite tm_size_power2. apply lt_split_bits.
   assumption. assumption. assumption.
+  replace (nth_error (tm_step m) (2^j)) with (nth_error (tm_step (S j)) (2^j)).
+  rewrite tm_build. rewrite nth_error_app2. rewrite tm_size_power2.
+  rewrite Nat.sub_diag. rewrite tm_step_head_1. simpl. reflexivity.
+  rewrite tm_size_power2. apply Nat.le_refl.
+  apply tm_step_stable. rewrite <- Nat.mul_1_l at 1.
+  rewrite Nat.pow_succ_r. rewrite <- Nat.mul_lt_mono_pos_r.
+  apply Nat.lt_1_2.
+  rewrite <- Nat.neq_0_lt_0. apply Nat.pow_nonzero. easy.
+  apply Nat.le_0_l. apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
+  assumption.
+  rewrite tm_step_head_1. simpl. reflexivity.
 
+  apply tm_step_stable.
+  generalize I. generalize H. generalize G. apply lt_split_bits.
+  assert (k*2^m + 2^j < 2^n).
+  generalize I. generalize H. generalize G. apply lt_split_bits.
+  assert (2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.
+  generalize H2. generalize H1. apply Nat.lt_le_trans.
 
-Lemma lt_split_bits : forall n m k j,
-  0 < k -> j < m -> k * 2^m < 2^n -> k * 2^m +2^j < 2^n.
-
-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)
+  apply tm_step_stable. assumption.
+  assert (2^n <= 2^(m+n)). apply Nat.pow_le_mono_r. easy. apply Nat.le_add_l.
+  generalize H1. generalize I. apply Nat.lt_le_trans.
+Qed.
 
 
 
-Theorem tm_step_stable : forall (n m k : nat),
-  k < 2^n -> k < 2^m -> nth_error (tm_step n) k = nth_error (tm_step m) k.
-
-
-
-
-Nat.mul_le_mono_nonneg:
-  forall n m p q : nat,
-  0 <= n -> n <= m -> 0 <= p -> p <= q -> n * p <= m * q
 
 
 Lemma tm_step_add_small_power2 :