Update

thue-morse.v

@@ -990,7 +990,59 @@ Proof.
     induction m.
     + rewrite Nat.add_0_r. rewrite Nat.add_0_r.
       rewrite H0. rewrite H1. inversion J. rewrite H3. reflexivity.
-    + 
+    +
+
+      assert (U: S k < 2^(S n+ m)).
+      assert (N: k < 2^n). apply I.
+      assert (L: 2^n < 2^(S n + m)).
+      assert (M: n < S n + m). rewrite Nat.add_succ_comm.
+      apply Nat.lt_add_pos_r. apply Nat.lt_0_succ.
+      apply Nat.pow_lt_mono_r. apply Nat.lt_1_2. apply M.
+      generalize L. generalize H. apply Nat.lt_trans.
+      assert (K := U). apply Nat.lt_succ_l in K.
+
+      assert (nth_error (tm_step n) k = Some (nth k (tm_step n) false)).
+      apply nth_error_nth'. rewrite tm_size_power2. apply I.
+      assert (nth_error (tm_step n) (S k) = Some (nth (S k) (tm_step n) false)).
+      apply nth_error_nth'. rewrite tm_size_power2. apply H.
+      rewrite <- H2 in J. rewrite <- H3 in J.
+
+      assert (nth_error (tm_step n) k = nth_error (tm_step (S n + m)) k).
+      generalize K. generalize I. apply tm_step_stable.
+      assert (nth_error (tm_step n) (S k) = nth_error (tm_step (S n + m)) (S k)).
+      generalize U. generalize H. apply tm_step_stable.
+
+      rewrite H4 in J. rewrite H5 in J.
+
+      assert (nth_error (tm_step (S n + m)) k = Some (nth k (tm_step (S n + m)) false)).
+      generalize K. rewrite <- tm_size_power2. apply nth_error_nth'.
+      assert (nth_error (tm_step (S n + m)) (S k) = Some (nth (S k) (tm_step (S n + m)) false)).
+      generalize U. rewrite <- tm_size_power2. apply nth_error_nth'.
+      rewrite H6 in J. rewrite H7 in J.
+      rewrite Nat.add_succ_comm in J. inversion J.
+
+
+      assert ( S k + 2^(n + S m) < 2^(S n + S m)
+  S k < 2^n ->
+    eqb (nth k (tm_step n) false) (nth (S k) (tm_step n) false)
+    = eqb
+
+      partir de H9 et appliquer :
+Lemma tm_step_next_range2_neighbor : forall (n 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 (S n)) false) (nth (S k + 2^n) (tm_step (S n)) false).
+
+
+      assert (nth_error (tm_step (S n + m)) (k + 2 ^ (n + m))
+                = nth_error (tm_step (S n + m)) (k + 2 ^ (n + m))
+
+
+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.
+
+
       assert (U: S k < 2^(S n+ m)).
       assert (N: k < 2^n). apply I.
       assert (L: 2^n < 2^(S n + m)).