diff --git a/src/thue_morse2.v b/src/thue_morse2.v
index d094e8d..d620783 100644
--- a/src/thue_morse2.v
+++ b/src/thue_morse2.v
@@ -12,6 +12,8 @@
    - tm_step_cubefree (there is no cube in the sequence)
    - tm_step_square_size (all squared factors of odd
      length have length 1 or 3).
+   - tm_step_square_pos (length of the prefix has the same
+     parity than the length of the factor being squared)
 *)  
 
 Require Import thue_morse.