baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-01-15 18:00:29 +01:00
parent 08b3a5dfbc
commit 0272aea248
1 changed files with 0 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/thue_morse2.v
View File

@ -1063,7 +1063,6 @@ Proof.
Qed.
Lemma tm_step_square_pos_even'' : forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ a ++ tl
-> 0 < length a
@ -1465,10 +1464,3 @@ Proof.
rewrite <- Nat.negb_odd. rewrite <- Nat.negb_odd.
rewrite H0. rewrite H1. reflexivity.
Qed.
(* TODO: la taille du facteur divise la taille du préfixe ? *)
(* TODO : le cas de la taille 2 est un cas pair facile
grâce à tm_step_factor4_odd_prefix *)
(* TODO: revoir tm_step_cube4 *)