From 6aa1efe86cc67abcf60cb09f8aadbac2a315e8a0 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Thu, 12 Jan 2023 18:37:20 +0100 Subject: [PATCH] Update --- src/thue_morse2.v | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) 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 *) + + +