This commit is contained in:
Thomas Baruchel 2023-01-12 18:37:20 +01:00
parent 6d0ee965ba
commit 6aa1efe86c

View File

@ -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 *)