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

Update

This commit is contained in:
Thomas Baruchel 2023-02-02 10:26:20 +01:00
parent 98843bb92d
commit 7b5ca73448
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/thue_morse3.v
View File

@ -2138,7 +2138,9 @@ Proof.
++ [b6; b5; b5; b3; b2; b1; b0; b] ++ tl)
with ((hd ++ [b; b0; b1; b2; b3; b5; b5; b6; b6])
++ [b5] ++ [b5] ++ [b3] ++ [b2;b1;b0;b] ++ tl) in H.
apply tm_step_cubefree in H.
apply tm_step_cubefree in H. destruct b5; destruct b3.
contradiction H. reflexivity. easy. easy. contradiction H. reflexivity.
apply Nat.lt_0_1. rewrite <- app_assoc. reflexivity.