Update

thue-morse.v

@@ -966,6 +966,45 @@ Proof.
     apply tm_step_next_range'.
 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.
+Proof.
+  intros n m k. intros.
+  assert (I: n < m /\ max n m = m \/ m <= n /\ max n m = n).
+  apply Nat.max_spec. destruct I.
+  - destruct H1. replace (m) with (n + (m-n)). apply tm_add_range. apply H.
+    apply Nat.lt_le_incl in H1. replace (m) with (n + m - n) at 2. generalize H1.
+    apply Nat.add_sub_assoc. rewrite Nat.add_comm.
+    assert (n <= n). apply le_n. symmetry.
+    replace (m) with (m + (n-n)) at 1. generalize H3.
+    apply Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_comm.
+    reflexivity.
+  - destruct H1. symmetry. replace (n) with (m + (n - m)). apply tm_add_range.
+    apply H0. replace (n) with (m + n - m) at 2. generalize H1.
+    apply Nat.add_sub_assoc. rewrite Nat.add_comm.
+    assert (m <= m). apply le_n. symmetry.
+    replace (n) with (n + (m-m)) at 1. generalize H3.
+    apply Nat.add_sub_assoc. rewrite Nat.sub_diag. rewrite Nat.add_comm.
+    reflexivity.
+Qed.
+
+
+
+Nat.add_sub_assoc: forall n m p : nat, p <= m -> n + (m - p) = n + m - p
+    rewrite <- H2. rewrite <- Nat.sub_max_distr_r. rewrite H2.
+    rewrite Nat.sub_diag. rewrite Nat.max_0_l.
+
+
+
+  assert (I: nth_error(tm_step (min n m)) k = nth_error (tm_step (max n m)) k).
+
+
+
+
+Nat.max_spec:
+  forall n m : nat, n < m /\ Nat.max n m = m \/ m <= n /\ Nat.max n m = n
+
+