diff --git a/src/thue_morse2.v b/src/thue_morse2.v
index c12fee5..1c81399 100644
--- a/src/thue_morse2.v
+++ b/src/thue_morse2.v
@@ -329,7 +329,9 @@ Qed.
 
 
 (**
-   New section
+   New following lemmas and theorems are related to the size
+   of squares in the Thue-Morse sequence, namely lengths of
+   2^n or 3 * 2^n only.
 *)
 
 Lemma tm_step_shift_odd_prefix_even_squares :
@@ -559,7 +561,7 @@ Qed.
 
 
 
-Lemma xxx : forall (n k j : nat) (hd a tl : list bool),
+Theorem tm_step_square_size : forall (n k j : nat) (hd a tl : list bool),
   tm_step (S n) = hd ++ a ++ a ++ tl
   -> length a = (S (Nat.double k)) * 2^j
   -> (k = 0 \/ k = 1).
@@ -602,15 +604,3 @@ Proof.
     rewrite <- app_assoc. reflexivity.
     generalize H2. apply IHj. easy.
 Qed.
-
-
-
-(*
-T[2:6] : carré (répété) de taille 2   (mais aussi T[10:14])
-T[4:12] : carré (répété) de taille 4   (mais aussi T[20:28])
-T[8:24] : carré (répété) de taille 8    (mais aussi T[40:56])
-
-Termes de 11 à 17 (exclus) : carré (répété) de taille 3
-Termes de 22 à 34 (exclus) : carré (répété) de taille 6
-Termes de 44 à 68 (exclus) : carré (répété) de taille 12
- *)