Update

thue-morse.v

@@ -904,7 +904,7 @@ Proof.
 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.
+  k < 2^n -> k < 2^m -> nth_error (tm_step n) k = nth_error (tm_step m) k.
 Proof.
   intros n m k. intros.
   assert (I: n < m /\ max n m = m \/ m <= n /\ max n m = n).
@@ -1089,11 +1089,30 @@ Lemma tm_step_cancel_high_bits :
       <-> odd n = true.
 Proof.
   intros k b n m. intros H I.
+  assert (J: nth_error (tm_step (S n)) (2^n-1) = nth_error (tm_step (S n)) (2^n)
+              <-> odd n = true).
+  assert (2^n - 1 < 2^n).
+  apply Nat.sub_lt. replace (1) with (2^0) at 1. apply Nat.pow_le_mono_r.
+  easy. apply le_0_n. simpl. reflexivity. apply Nat.lt_0_1.
+  rewrite tm_step_single_bit_index.
+  assert (nth_error (tm_step n) (2^n - 1) = nth_error (tm_step (S n)) (2^n-1)).
+  apply tm_step_stable. apply H0.
+  assert (2^n < 2^(S n)). apply Nat.pow_lt_mono_r. apply Nat.lt_1_2.
+  apply Nat.lt_succ_diag_r.
+  generalize H1. generalize H0. apply Nat.lt_trans. rewrite <- H1.
+  rewrite tm_step_repunit_index.
+
+  rewrite Nat.succ_lt_mono. simpl.
   (*
   assert (K: nth_error (tm_step n) a = Some (odd n)). rewrite I.
   apply tm_step_repunit.
    *)
-
+  
+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.
+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.