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-22 15:48:06 +01:00
parent 775f08c49c
commit 7cc18437c9
1 changed files with 10 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/thue_morse3.v
View File

@ -802,6 +802,16 @@ Le lemme repeating_patterns se base sur les huit premiers termes de TM :
replace 8 with (2^3). rewrite <- Nat.pow_lt_mono_r_iff.
assumption. apply Nat.lt_1_2. reflexivity.
(* termes à prouver *)
assert (U:
nth_error (b3 :: b5 :: b7 :: hd) (length (b3 :: b5 :: b7 :: hd) - 3)
= Some b8). unfold b8.
rewrite app_removelast_last with (l := b3::b5::b7::hd) (d := false) at 1.
rewrite app_removelast_last
with (l := (removelast (b3::b5::b7::hd))) (d := false) at 1.
rewrite app_removelast_last
with (l := (removelast (removelast (b3::b5::b7::hd)))) (d := false) at 1.
rewrite <- app_assoc. rewrite <- app_assoc. rewrite nth_error_app2.