Update

thue-morse.v

@@ -316,55 +316,34 @@ Proof.
   intro n.
   induction n.
   - reflexivity.
-  - rewrite tm_build. rewrite app_length. rewrite map_length.
-    replace (2^S n) with (2^n + 2^n). rewrite IHn. reflexivity.
-    simpl. rewrite <- plus_n_O. reflexivity.
+  - rewrite <- tm_step_lemma. rewrite tm_morphism_size.
+    rewrite Nat.pow_succ_r. rewrite Nat.mul_cancel_l.
+    assumption. easy. apply Nat.le_0_l.
 Qed.
 
-Lemma tm_step_head_2 : forall (n : nat),
-    tm_step (S n) = false :: true :: tl (tl (tm_step (S n))).
-Proof.
-  intro n.
-  induction n.
-  - reflexivity.
-  - simpl. replace (tm_morphism (tm_step n)) with (tm_step (S n)).
-    rewrite IHn. reflexivity. reflexivity.
-Qed.
-
-Lemma tm_step_end_2 : forall (n : nat),
-  rev (tm_step (S n)) = even n :: odd n :: tl (tl (rev (tm_step (S n)))).
-Proof.
-  intro n. induction n.
-  - reflexivity.
-  - simpl tm_step. rewrite tm_morphism_rev.
-    replace (tm_morphism (tm_step n)) with (tm_step (S n)).
-    rewrite IHn. simpl tm_morphism. simpl tl.
-    rewrite Nat.even_succ.
-    rewrite Nat.odd_succ.
-    rewrite negb_involutive.
-    reflexivity. reflexivity.
-Qed.
 
 Lemma tm_step_head_1 : forall (n : nat),
     tm_step n = false :: tl (tm_step n).
 Proof.
   intro n. 
-  destruct n.
+  induction n.
   - reflexivity.
-  - rewrite tm_step_head_2. reflexivity.
+  - rewrite <- tm_step_lemma. rewrite IHn. reflexivity.
 Qed.
 
+
 Lemma tm_step_end_1 : forall (n : nat),
   rev (tm_step n) = odd n :: tl (rev (tm_step n)).
 Proof.
   intro n.
-  destruct n.
+  induction n.
   - reflexivity.
-  - rewrite tm_step_end_2. simpl.
-    rewrite Nat.odd_succ.
-    reflexivity.
+  - rewrite <- tm_step_lemma. rewrite tm_morphism_rev.
+    rewrite IHn. simpl. rewrite <- Nat.negb_even at 1. rewrite Nat.odd_succ.
+    rewrite negb_involutive. reflexivity.
 Qed.
 
+
 Theorem tm_step_double_index : forall (n k : nat),
   nth_error (tm_step n) k = nth_error (tm_step (S n)) (2*k).
 Proof.