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-14 21:03:04 +01:00
parent aae08b747a
commit 3c2f4121e1
2 changed files with 4 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/thue_morse.v
View File

@ -413,7 +413,7 @@ Proof.
apply tm_step_count_occ.
rewrite count_occ_app in L. rewrite count_occ_app in L.
rewrite K in L. rewrite Nat.add_cancel_l in L.
destruct b; simpl in L; inversion L.
destruct b; inversion L.
Qed.
Lemma tm_step_consecutive_identical' :

4
src/thue_morse2.v
View File

@ -515,5 +515,7 @@ Proof.
(* TODO: utiliser tm_step_odd_prefix_square pour le cas impair *)
(* 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 *)
Admitted.