Update

src/thue_morse.v

@@ -1,4 +1,5 @@
-(**
+(** * The Thue-Morse sequence
+
    Some proofs related to the Thue-Morse sequence.
    See:
    - https://oeis.org/A010060
@@ -123,15 +124,17 @@ Proof.
     rewrite negb_involutive. reflexivity.
 Qed.
 
-Lemma tm_morphism_rev' : forall (l : list bool),
-  rev (tm_morphism l) = map negb (tm_morphism (rev l)).
+
+Lemma tm_build_negb : forall (l : list bool),
+  tm_morphism (map negb l) = map negb (tm_morphism l).
 Proof.
-  intro l. rewrite tm_morphism_rev. induction l.
+  intro l.
+  induction l.
   - reflexivity.
-  - simpl. rewrite map_app. rewrite tm_morphism_concat. rewrite IHl.
-    rewrite tm_morphism_concat. rewrite map_app. reflexivity.
+  - simpl. rewrite IHl. reflexivity.
 Qed.
 
+
 Lemma tm_morphism_double_index : forall (l : list bool) (k : nat),
   nth_error l k = nth_error (tm_morphism l) (2*k).
 Proof.
@@ -149,15 +152,6 @@ Proof.
       reflexivity.
 Qed.
 
-Lemma tm_build_negb : forall (l : list bool),
-  tm_morphism (map negb l) = map negb (tm_morphism l).
-Proof.
-  intro l.
-  induction l.
-  - reflexivity.
-  - simpl. rewrite IHl. reflexivity.
-Qed.
-
 
 Lemma tm_morphism_count_occ : forall (l : list bool),
   count_occ Bool.bool_dec (tm_morphism l) true
@@ -298,9 +292,9 @@ Theorem tm_step_negb : forall (n : nat),
 Proof.
   intro n.
   rewrite <- tm_step_lemma. symmetry.
-  replace (tm_step n) with (rev (rev (tm_step n))).
-  rewrite rev_involutive. rewrite tm_morphism_rev'. reflexivity.
-  rewrite rev_involutive. reflexivity.
+  replace (tm_step n) with (rev (rev (tm_step n))); rewrite rev_involutive.
+  - rewrite tm_morphism_rev. rewrite tm_build_negb. reflexivity.
+  - reflexivity.
 Qed.
 
 Theorem tm_build : forall (n : nat),