diff --git a/src/thue_morse2.v b/src/thue_morse2.v index 47716f6..6aaeff5 100644 --- a/src/thue_morse2.v +++ b/src/thue_morse2.v @@ -729,13 +729,6 @@ Proof. Qed. - - - - - - - Theorem tm_step_square_pos_even : forall (n : nat) (hd a tl : list bool), tm_step n = hd ++ a ++ a ++ tl -> 0 < length a -> even (length (hd ++ a)) = true. @@ -749,3 +742,7 @@ Proof. + (* TODO: utiliser tm_step_odd_prefix_square pour le cas impair *) + + +