Update

thue-morse.v

@@ -903,6 +903,7 @@ Proof.
   rewrite tm_size_power2. apply Nat.le_add_l.
 Qed.
 
+(*
 Theorem tm_fullrange : forall (n m k : nat),
   k < 2^n -> k < 2^m -> nth_error (tm_step n) k = nth_error (tm_step m) k.
 Proof.
@@ -911,13 +912,26 @@ Proof.
   - destruct m. reflexivity. simpl in H. rewrite Nat.lt_1_r in H. rewrite H. 
     replace (tm_step (S m)) with (false :: tl (tm_step (S m))). reflexivity.
     symmetry. apply tm_step_head_1.
-  - induction m. simpl in H0. rewrite Nat.lt_1_r in H0. rewrite H0.
+  -  (* prouver d'abord que k < 2^n !!! *)
+    assert (I := H0). rewrite <- tm_size_power2 in I.
+    rewrite <- nth_error_Some in I.
+
+
+
+
+  - destruct m. simpl in H0. rewrite Nat.lt_1_r in H0. rewrite H0.
     replace (tm_step (S n)) with (false :: tl (tm_step (S n))). reflexivity.
     symmetry. apply tm_step_head_1.
 
 
 
 
+    assert (nth_error (tm_step (S n)) k = nth_error (tm_step m) k).
+    apply IHm.
+
+
+
+
 
 
 
@@ -936,6 +950,22 @@ 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_add_range : forall (n m k : nat),
+  k < 2^n -> nth_error (tm_step n) k = nth_error (tm_step (n+m)) k.
+Proof.
+  intros n m k. intros H.
+  induction m.
+  - rewrite Nat.add_comm. reflexivity.
+  - rewrite Nat.add_succ_r. rewrite <- tm_size_power2 in H.
+    assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
+    generalize H. apply nth_error_nth'.
+    rewrite H0 in IHm. symmetry in IHm.
+    rewrite H0. symmetry. generalize IHm.
+    apply tm_step_next_range'.
+Qed.
+