diff --git a/src/thue_morse3.v b/src/thue_morse3.v
index 931fe0f..811d15e 100644
--- a/src/thue_morse3.v
+++ b/src/thue_morse3.v
@@ -1357,7 +1357,8 @@ Proof.
 Qed.
 
 
-Theorem tm_step_palindromic_length_12_n :
+(* TODO: this theorem could be made more powerful with 2 < n *)
+Lemma tm_step_palindromic_length_12_n :
   forall (n : nat) (hd a tl : list bool),
   tm_step n = hd ++ a ++ (rev a) ++ tl
   -> length a > 6
@@ -1410,7 +1411,22 @@ Proof.
   assert (L: length (hd ++ a ++ rev a ++ tl) mod 4 = 0).
   rewrite <- H. rewrite tm_size_power2.
 
-Admitted.
+  assert (V: 1 < n). generalize I. generalize H.
+  apply tm_step_palindromic_length_12_n.
+  destruct n. inversion V. destruct n. inversion V. inversion H1.
+  rewrite Nat.pow_succ_r. rewrite Nat.pow_succ_r.
+  rewrite Nat.mul_comm. rewrite <- Nat.mul_assoc.
+  rewrite Nat.mul_comm. rewrite <- Nat.mul_assoc.
+  apply Nat.mod_mul. easy. apply le_0_n. apply le_0_n.
+
+  rewrite app_length in L.
+  rewrite <- Nat.add_mod_idemp_l in L. rewrite K in L.
+  rewrite app_length in L. rewrite Nat.add_0_l in L.
+  rewrite <- Nat.add_mod_idemp_l in L. rewrite J in L.
+  rewrite Nat.add_0_l in L. rewrite app_length in L.
+  rewrite <- Nat.add_mod_idemp_l in L. rewrite rev_length in L.
+  rewrite J in L. assumption. easy. easy. easy.
+Qed.
 
 Lemma tm_step_palindromic_even_morphism1 :
   forall (n : nat) (hd a tl : list bool),