Update

src/thue_morse.v

@@ -375,6 +375,23 @@ Proof.
     rewrite tm_size_power2. apply Nat.pow_nonzero. easy.
 Qed.
 
+Theorem tm_step_count_occ : forall (hd tl : list bool) (n : nat),
+  tm_step n = hd ++ tl -> even (length hd) = true
+  -> count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false.
+Proof.
+  intros hd tl n. intros H I.
+  destruct n.
+  - assert (J: hd = nil). destruct hd. reflexivity.
+    simpl in H. inversion H.
+    symmetry in H2. apply app_eq_nil in H2.
+    destruct H2. rewrite H0 in I. simpl in I. inversion I.
+    rewrite J. reflexivity.
+  - rewrite <- tm_step_lemma in H.
+    assert (J: hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
+    generalize I. generalize H. apply tm_morphism_app2.
+    rewrite J. apply tm_morphism_count_occ.
+Qed.
+
 
 (**
    The following lemmas and theorems focus on the stability of the sequence:
@@ -891,23 +908,6 @@ Qed.
    lemmas are defined for the very specific purpose of being used in the
    final proof.
 *)
-Theorem tm_step_count_occ : forall (hd tl : list bool) (n : nat),
-  tm_step n = hd ++ tl -> even (length hd) = true
-  -> count_occ Bool.bool_dec hd true = count_occ Bool.bool_dec hd false.
-Proof.
-  intros hd tl n. intros H I.
-  destruct n.
-  - assert (J: hd = nil). destruct hd. reflexivity.
-    simpl in H. inversion H.
-    symmetry in H2. apply app_eq_nil in H2.
-    destruct H2. rewrite H0 in I. simpl in I. inversion I.
-    rewrite J. reflexivity.
-  - rewrite <- tm_step_lemma in H.
-    assert (J: hd = tm_morphism (firstn (Nat.div2 (length hd)) (tm_step n))).
-    generalize I. generalize H. apply tm_morphism_app2.
-    rewrite J. apply tm_morphism_count_occ.
-Qed.
-
 
 Lemma tm_step_cube1 : forall (n : nat) (a hd tl: list bool),
   tm_step n = hd ++ a ++ a ++ a ++ tl -> even (length a) = true.
@@ -1350,3 +1350,13 @@ Proof.
 Qed.
 
 
+
+
+
+
+
+(**
+   Under construction
+*)
+
+